From 99dfe084040cd5e3d4924f7d70cb90cfb1633153 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 30 Nov 2024 17:38:22 -0500 Subject: [PATCH] Set implicitLambda to false when elaborating terms passed into Duper --- Duper/Tactic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean index eca30e7..968731a 100644 --- a/Duper/Tactic.lean +++ b/Duper/Tactic.lean @@ -149,7 +149,7 @@ def elabFact (stx : Term) : TacticM (Array (Expr × Expr × Array Name)) := do where elabFactAux (stx : Term) : TacticM (Expr × Expr × Array Name) := -- elaborate term as much as possible and abstract any remaining mvars: Term.withoutModifyingElabMetaStateWithInfo <| withRef stx <| Term.withoutErrToSorry do - let e ← Term.elabTerm stx none + let e ← Term.elabTerm stx none (implicitLambda := false) Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true) let e ← instantiateMVars e let abstres ← Duper.abstractMVars e