search

wilbowma / cur

A less devious proof assistant
BSD 2-Clause "Simplified" License
222 stars 18 forks source link

Reimplement pattern matching #55

Closed wilbowma closed 4 years ago

wilbowma commented 8 years ago

Make it not a giant hack.

Support nested pattern matching. See pattern matricies literature on how to compile these to trivial patterns.

www.irif.univ-paris-diderot.fr/~sozeau/research/publications/Equations:_A_Dependent_Pattern-Matching_Compiler.pdf

wilbowma commented 6 years ago

See also #66 and #77

wilbowma commented 6 years ago

Thanks to @stchang, this is getting rewritten in the turnstile-core branch.