JetBrains / Arend

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

Wrong scopes for `\data` defined with `\with` construction #332

Closed sxhya closed 1 year ago

sxhya commented 1 year ago

In the following example you will get multiple Cannot resolve reference 'X' errors, which can be fixed by replacing \with with \elim n:

\data Foo {X : \Type} (n : Nat) \with
  | zero => nil X
  | suc n => cons X (Foo {X} n)
valis commented 1 year ago

Not a bug