Zulip Chat Archive

Stream: general

Topic: instance transparency


view this post on Zulip Floris van Doorn (Dec 24 2020 at 02:34):

In docs#tactic.transparency there are 5 transparency settings:

all : tactic.transparency
semireducible : tactic.transparency
instances : tactic.transparency
reducible : tactic.transparency
none : tactic.transparency

I always thought that the lower transparency settings always involved fewer declarations. However, I just noticed that the instances transparency even applies to instances that are marked @[irreducible] (which means it applies to some definitions that semireducible doesn't apply to):

@[irreducible] instance has_zero.bool : has_zero bool :=
{ zero := ff }

open tactic
run_cmd do
e  to_expr ``(0 : bool),
trace e, -- 0
e2  whnf e transparency.instances,
trace e2, -- ff
e3  whnf e transparency.semireducible,
trace e3, -- 0
skip

Is this intended? It sounds unwanted - I think of the instance transparency to unfold slightly more definitions than the reducible ones.
Background: I tried adding @[simps] to docs#category_theory.iso.op, but this gives an error, because @[simps] has unfolded the (irreducible) type when applying whnf ... transparency.instances to the type.

view this post on Zulip Floris van Doorn (Mar 05 2021 at 04:28):

This is fixed in lean#538. Thanks @Gabriel Ebner!


Last updated: May 09 2021 at 19:11 UTC