search

JetBrains / Arend

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

Infer (class of (parameters of (functions defined in instances))) #265

Open tonyxty opened 4 years ago

tonyxty commented 4 years ago

Example:

\class B
  | v : Nat

\class C
  | f (x : B) : B

\instance inst : C
  | f x => \new B {
    | v => suc (x.v)  -- but currently we have to write (B.v {x})
  }

This might be related to #126.

ice1000 commented 4 years ago

Temporary workaround: adding type annotation to x

ice1000 commented 4 years ago 
\instance inst : C
  | f (x : B) => \new B {
    | v => suc (x.v)
  }
valis commented 4 years ago

Do you want to write x.v or just v? The title of the issue makes me think that you want the latter, but the text itself has the former option.

tonyxty commented 4 years ago

Do you want to write x.v or just v? The title of the issue makes me think that you want the latter, but the text itself has the former option.

Alas, human language. I've edited the title, hopefully it's clearer now.