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

fix: trace message with incorrect MetavarContext

Browse source
This commit is contained in:
Leonardo de Moura 2022-01-24 10:34:44 -08:00
parent 7ada79bf2e
commit 722bf54929
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/Meta/SynthInstance.lean
View file

@ -409,7 +409,7 @@ private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
And then, store it in the tabled entries map, and wakeup waiters. -/
def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
if cNode.size ≥ (← read).maxResultSize then
traceM `Meta.synthInstance.discarded do m!"size: {cNode.size} ≥ {(← read).maxResultSize}, {← inferType cNode.mvar}"
traceM `Meta.synthInstance.discarded do withMCtx cNode.mctx do m!"size: {cNode.size} ≥ {(← read).maxResultSize}, {← inferType cNode.mvar}"
return ()
else
let answer ← mkAnswer cNode