search

aya-prover / aya-dev

A proof assistant and a dependently-typed language
https://www.aya-prover.org
MIT License
281 stars 16 forks source link

Array exprs need a checking mode #1145

Closed ice1000 closed 1 day ago

ice1000 commented 1 day ago

So if the type info is clear, it should apply checking mode rules.