search

JetBrains / Arend

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

Unification enhancement #243

Closed ice1000 closed 4 years ago

ice1000 commented 4 years ago

Suppose we have the code example in #242.

If we replace the B type parameter in Reveal with a dependent version (say, A -> \Type), it won't the inferred in inspect. So, the following code will cause an error:

\record Reveal {A : \Type} {B : A -> \Type} (f : \Pi (a : A) -> B a) (x : A) (y : B)
  | eq : f x = y

\func inspect {A : \Type} {B : A -> \Type} (f : \Pi (a : A) -> B a) : Reveal f x (f x) \cowith
  | eq => idp
valis commented 4 years ago

I don't understand this code, but I don't think we need this at all. See comment in #242.

ice1000 commented 4 years ago

Yes, you're right