Revision 7d48561a5e49429f02d1bfe35bc7c32be85096ac authored by Pierre-Yves Strub on 05 April 2024, 11:33:24 UTC, committed by Pierre-Yves Strub on 05 April 2024, 11:50:31 UTC
This diff removes all the corner cases of the matching algorithm.

The matching algorithm is now full-duplex (before, only the
pattern was allowed to contain match variables)

Matching performance is identical (test done on the examples &
the standard library)

Previous implementation was missing some trivial matching and
the refactoring solves this issue. Some proofs might have to
be fixed.
1 parent 41c2667
Raw File
.gitignore
*~

*.pyc
*.pyo

/_build
/result
/etc
/theories/attic

/ec.*
/src/*.exe

*.eco

/*.ec
/*.eca
/*.smt
/*.why

.merlin
*.install
*.log
back to top