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

fix: make InteractiveHyp.fvarIds optional

Browse source 
This is for backwards compat.
This commit is contained in:
E.W.Ayers 2022-06-01 09:53:43 -04:00 • committed by Leonardo de Moura
parent 0f61d1dc59
commit 675147dcfc
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
names : Array String
fvarIds : Array FVarId
fvarIds? : Option (Array FVarId)
type : CodeWithInfos
val? : Option CodeWithInfos := none
isInstance : Bool