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

fix: leaking isDefEqStuckExceptionId

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-25 18:41:17 -07:00
parent 8e159f004c
commit 27be7e6812
1 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Lean/Meta/SynthInstance.lean
View file

@ -579,11 +579,14 @@ catchInternalId isDefEqStuckExceptionId
(toLOptionM $ synthInstanceImp? type)
(fun _ => pure LOption.undef)
private def synthInstanceImp (type : Expr) : MetaM Expr := do
result? ← synthInstanceImp? type;
match result? with
| some result => pure result
| none => throwError $ "failed to synthesize" ++ indentExpr type
private def synthInstanceImp (type : Expr) : MetaM Expr :=
catchInternalId isDefEqStuckExceptionId
(do
result? ← synthInstanceImp? type;
match result? with
| some result => pure result
| none => throwError $ "failed to synthesize" ++ indentExpr type)
(fun _ => throwError $ "failed to synthesize" ++ indentExpr type)
private def synthPendingImp (mvarId : MVarId) : MetaM Bool := do
mvarDecl ← getMVarDecl mvarId;
@ -593,7 +596,7 @@ match mvarDecl.kind with
match c? with
| none => pure false
| some _ => do
val? ← synthInstanceImp? mvarDecl.type;
val? ← catchInternalId isDefEqStuckExceptionId (synthInstanceImp? mvarDecl.type) (fun _ => pure none);
match val? with
| none => pure false
| some val =>