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.

Sign up for GitHub

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

Jump to bottom

Compiler error with underapplied projections in TC instances #2096

Open
gebner opened this issue Feb 6, 2023 · 1 comment
Open

Compiler error with underapplied projections in TC instances #2096

gebner opened this issue Feb 6, 2023 · 1 comment
Labels
bug Something isn't working depends on new code generator We are currently working on a new compiler (code generator) for Lean. This issue/PR is blocked by it

Comments

@gebner
Copy link
Member

gebner commented Feb 6, 2023 

instance : Coe { p : Nat → Prop // p 42 } (Nat → Prop) where
  coe := Subtype.val

fails with:
error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Subtype.val', and it does not have executable code

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/noncomputable/near/326249302
@gebner gebner added bug Something isn't working depends on new code generator We are currently working on a new compiler (code generator) for Lean. This issue/PR is blocked by it labels Feb 6, 2023
@gebner
Copy link
Member Author

gebner commented Feb 6, 2023

As a workaround, you can write coe x := x.val for the time being.

@gebner gebner mentioned this issue Feb 10, 2023
Open
@gebner gebner mentioned this issue Apr 21, 2023
Closed
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this issue Apr 22, 2023
@gebner
fix: computable KleeneAlgebra (Language α) instance (#3585)
754c3ef 
This is another case of leanprover/lean4#2096
kbuzzard pushed a commit to leanprover-community/mathlib4 that referenced this issue Apr 22, 2023
@gebner @kbuzzard
fix: computable KleeneAlgebra (Language α) instance (#3585)
f34f8ee 
This is another case of leanprover/lean4#2096
semorrison pushed a commit to leanprover-community/mathlib4 that referenced this issue May 10, 2023
@gebner
fix: computable KleeneAlgebra (Language α) instance (#3585)
43d4e83 
This is another case of leanprover/lean4#2096
hrmacbeth pushed a commit to leanprover-community/mathlib4 that referenced this issue May 10, 2023
@gebner @hrmacbeth
fix: computable KleeneAlgebra (Language α) instance (#3585)
e2bd060 
This is another case of leanprover/lean4#2096
hrmacbeth pushed a commit to leanprover-community/mathlib4 that referenced this issue May 11, 2023
@gebner @hrmacbeth
fix: computable KleeneAlgebra (Language α) instance (#3585)
add69d9 
This is another case of leanprover/lean4#2096
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working depends on new code generator We are currently working on a new compiler (code generator) for Lean. This issue/PR is blocked by it
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@gebner