Closed strub closed 7 months ago
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.
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.