Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
tonyxty opened this issue Sep 26, 2020 · 4 comments
Open

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

tonyxty opened this issue Sep 26, 2020 · 4 comments
Labels

Comments

@tonyxty
Copy link

tonyxty commented Sep 26, 2020

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
Copy link
Contributor

ice1000 commented Sep 26, 2020

Temporary workaround: adding type annotation to x

@ice1000
Copy link
Contributor

ice1000 commented Sep 26, 2020

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

@valis
Copy link
Collaborator

valis commented Sep 28, 2020

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 tonyxty changed the title Infer class of parameters of functions defined in instances Infer (class of (parameters of (functions defined in instances))) Sep 29, 2020
@tonyxty
Copy link
Author

tonyxty commented Sep 29, 2020

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

3 participants