search

JetBrains / Arend

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

Problem with mixing constructors defined via pattern-matching with external parameters #339

Closed sxhya closed 6 months ago

sxhya commented 10 months ago 
\func f {X : \Type} => X \where {
  \data D1 (n : Nat) \with
    | 0 => nilD X -- 'X' is not a reference to either a definition or a variable
}

\func f2 {X : \Type} => X \where {
  \data D2 (n : Nat)
    | nilD2 X -- No error
}