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