search

JetBrains / Arend

The Arend Proof Assistant
https://arend-lang.github.io/
Apache License 2.0
694 stars 33 forks source link

Number type-checker for patterns and copatterns #231

Closed valis closed 4 years ago

valis commented 4 years ago

Number literals can appear in patterns, but number type-checker is not invoked there. We can also allow numbers in copatterns and invoke it there too.

ice1000 commented 4 years ago

Do we have language extension for patterns?

valis commented 4 years ago

Number typechecker is not invoked in patterns. That's a part of this task.