search

polarity-lang / polarity

A Language with Dependent Data and Codata Types
https://polarity-lang.github.io
Apache License 2.0
50 stars 0 forks source link

Remove the omit_absurd feature #252

Closed BinderDavid closed 3 months ago

BinderDavid commented 3 months ago

This allows to simplify the implementation of the elaborator for matches and comatches. I have also factored the exhaustiveness checking into separate functions.