Arend icon indicating copy to clipboard operation
Arend copied to clipboard

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

Open tonyxty opened this issue 4 years ago • 4 comments

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.

tonyxty avatar Sep 26 '20 18:09 tonyxty

Temporary workaround: adding type annotation to x

ice1000 avatar Sep 26 '20 23:09 ice1000

\instance inst : C
  | f (x : B) => \new B {
    | v => suc (x.v)
  }

ice1000 avatar Sep 26 '20 23:09 ice1000

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.

valis avatar Sep 28 '20 20:09 valis

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.

tonyxty avatar Sep 29 '20 05:09 tonyxty