From c474dff38c401723226277240cd3baec0437de15 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 7 Dec 2023 17:04:40 +0000 Subject: [PATCH] doc: document constructors of `TransparencyMode` (#3037) Taken from https://github.com/leanprover-community/lean4-metaprogramming-book/blob/master/md/main/04_metam.md#transparency I can never remember which way around `reducible` and `default` go, and this avoids me needing to leave the editor to find out. --- src/Init/MetaTypes.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index 2c5a49524e..5b4158c320 100644 --- a/src/Init/MetaTypes.lean +++ b/src/Init/MetaTypes.lean @@ -21,7 +21,14 @@ structure Module where namespace Meta inductive TransparencyMode where - | all | default | reducible | instances + /-- unfold all constants, even those tagged as `@[irreducible]`. -/ + | all + /-- unfold all constants except those tagged as `@[irreducible]`. -/ + | default + /-- unfold only constants tagged with the `@[reducible]` attribute. -/ + | reducible + /-- unfold reducible constants and constants tagged with the `@[instance]` attribute. -/ + | instances deriving Inhabited, BEq inductive EtaStructMode where