Arend
Arend copied to clipboard
Infer (class of (parameters of (functions defined in instances)))
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.
Temporary workaround: adding type annotation to x
\instance inst : C
| f (x : B) => \new B {
| v => suc (x.v)
}
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.
Do you want to write
x.v
or justv
? 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.