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

doc: ToHide.collect

Browse source
This commit is contained in:
E.W.Ayers 2022-05-27 17:39:06 -04:00 • committed by Leonardo de Moura
parent 6e1c9653d9
commit 4165b7e8ba
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -131,7 +131,8 @@ private def getInitialHiddenInaccessible (propOnly : Bool) : MetaM FVarIdSet :=
/-
If pp.inaccessibleNames == false, then collect two sets of `FVarId`s : `hiddenInaccessible` and `hiddenInaccessibleProp`
1- `hiddenInaccessible` contains `FVarId`s of free variables with inaccessible names that
a) are not propositions or are propositions containing "visible" names.
a) are not propositions or
b) are propositions containing "visible" names.
2- `hiddenInaccessibleProp` contains `FVarId`s of free variables with inaccessible names that are propositions
containing "visible" names.
Both sets do not contain `FVarId`s that contain visible backward or forward dependencies.