From 4165b7e8ba83369a5a7e9d2a05de237e18b5d357 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Fri, 27 May 2022 17:39:06 -0400 Subject: [PATCH] doc: ToHide.collect --- src/Lean/Meta/PPGoal.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean index 56d96f8724..004ff02b0f 100644 --- a/src/Lean/Meta/PPGoal.lean +++ b/src/Lean/Meta/PPGoal.lean @@ -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.