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

feat: instantiateMVars when formatting messages

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-05 07:02:28 -08:00
parent 9715bc7738
commit 0f1184e1d6
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/Init/Lean/Util/Message.lean
View file

@ -49,7 +49,7 @@ partial def formatAux : Option (Environment × MetavarContext × LocalContext)
| _, ofLevel u => fmt u
| _, ofName n => fmt n
| none, ofExpr e => format (toString e)
| some (env, mctx, lctx), ofExpr e => format (toString e) -- TODO: invoke pretty printer
| some (env, mctx, lctx), ofExpr e => format (toString (mctx.instantiateMVars e).1) -- TODO: invoke pretty printer
| _, context env mctx lctx d => formatAux (some (env, mctx, lctx)) d
| ctx, tagged cls d => Format.sbracket (format cls) ++ " " ++ formatAux ctx d
| ctx, nest n d => Format.nest n (formatAux ctx d)