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

fix: add missing instantiateMVars

Browse source
This commit is contained in:
Wojciech Nawrocki 2023-06-26 15:36:49 -07:00 • committed by Leonardo de Moura
parent d54ecc4373
commit ba4bfe26f2
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/Server/FileWorker/WidgetRequests.lean
View file

@ -49,7 +49,7 @@ def makePopup : WithRpcRef InfoWithCtx → RequestM (RequestTask InfoPopup)
| ⟨i⟩ => RequestM.asTask do
i.ctx.runMetaM i.info.lctx do
let type? ← match (← i.info.type?) with
| some type => some <$> ppExprTagged type
| some type => some <$> (ppExprTagged =<< instantiateMVars type)
| none => pure none
let exprExplicit? ← match i.info with
| Elab.Info.ofTermInfo ti =>