Zulip Chat Archive
Stream: general
Topic: instance search + semireducible
Reid Barton (May 19 2020 at 16:33):
While we're on a nearby topic, I've been meaning to ask: is it still the plan for Lean 4 to use semireducible transparency when deciding whether to apply an instance? (@Sebastian Ullrich?)
This would be a pretty significant change to certain parts of mathlib, and I'd like to start exploring the consequences of such a change, but I don't want to do it if it's not actually going to happen.
Reid Barton (May 19 2020 at 16:35):
(My Lean 4 build is now failing for reasons apparently unrelated to cmake
, so I figured it's easiest to just ask.)
Sebastien Gouezel (May 19 2020 at 16:44):
Currently, Lean 3 is not even using the instances
transparency flag and falls back to reducible
(see lean#244), so this would be a pretty big change indeed.
Reid Barton (May 19 2020 at 16:55):
Hmm, I guess that must only happen in sufficiently complicated situations (which is consistent with the linked Zulip discussion) because I know I have seen examples where instance search can unfold the definitions of instances.
Sebastian Ullrich (May 20 2020 at 10:01):
Reid Barton said:
While we're on a nearby topic, I've been meaning to ask: is it still the plan for Lean 4 to use semireducible transparency when deciding whether to apply an instance?
I don't know/remember anything about that. https://github.com/leanprover/lean4/blob/master/src/Init/Lean/Meta/SynthInstance.lean#L545
Reid Barton (May 20 2020 at 11:03):
Hmm, thanks. Maybe it was a short-lived idea.
Last updated: Dec 20 2023 at 11:08 UTC