max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: generalize withPPInaccessibleNames

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-15 18:58:06 -07:00
parent 4dabfef0e3
commit 4b69193442
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Meta/PPGoal.lean
View file

@ -20,9 +20,12 @@ register_builtin_option pp.inaccessibleNames : Bool := {
descr := "display inaccessible declarations in the local context"
}
def withPPInaccessibleNames (x : MetaM α) (flag := true) : MetaM α :=
def withPPInaccessibleNamesImp (flag : Bool) (x : MetaM α) : MetaM α :=
withTheReader Core.Context (fun ctx => { ctx with options := pp.inaccessibleNames.setIfNotSet ctx.options flag }) x
def withPPInaccessibleNames [MonadControlT MetaM m] [Monad m] (x : m α) (flag := true) : m α :=
mapMetaM (withPPInaccessibleNamesImp flag) x
namespace ToHide
structure State where