Zulip Chat Archive
Stream: mathlib4
Topic: noncomputable
Yury G. Kudryashov (Feb 06 2023 at 22:21):
I'm porting topology.sets.opens !4#2118, and Lean claims that the Coe instance is noncomputable. Why?
Yury G. Kudryashov (Feb 06 2023 at 22:33):
@Mario Carneiro @Gabriel Ebner :up:
Eric Wieser (Feb 06 2023 at 22:38):
the error GitHub links are broken
Gabriel Ebner (Feb 06 2023 at 22:38):
That looks like a compiler bug with underapplied Subtype.val.
Gabriel Ebner (Feb 06 2023 at 22:38):
If you write coe x := x.val instead of coe := Subtype.val, the error goes away.
Gabriel Ebner (Feb 06 2023 at 22:43):
Filed as lean4#2096. Don't expect it to be fixed any time soon.
Yury G. Kudryashov (Feb 10 2023 at 20:30):
I have several more strange noncomputables in !4#2174 (e.g., Union instance on bundled measurable sets)
Yury G. Kudryashov (Feb 10 2023 at 20:30):
@Gabriel Ebner :up:
Yury G. Kudryashov (Feb 10 2023 at 20:31):
I don't care about computability of these definitions, just want to know if this is the same bug or not.
Gabriel Ebner (Feb 10 2023 at 20:46):
I think they're related issues, but I've filed it as lean4#2104 so that we can close more bugs when the new compiler lands. :smirk:
Last updated: Dec 20 2023 at 11:08 UTC