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

doc: src/Lean/Widget/InteractiveGoal.lean

Browse source 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This commit is contained in:
Ed Ayers 2022-06-10 12:41:18 -04:00 • committed by Leonardo de Moura
parent cea53fc53e
commit 5130da82a8
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Widget/InteractiveGoal.lean
View file

@ -14,7 +14,7 @@ open Server
structure InteractiveHypothesis where
/-- The user-friendly name for each hypothesis.
If anonymous then the name is inaccessible. -/
If anonymous then the name is inaccessible and hidden. -/
names : Array Name
fvarIds? : Option (Array FVarId)
type : CodeWithInfos