Skip to content

Commit

Permalink
Adding @ before elaborating input fact syntax
Browse files Browse the repository at this point in the history
  • Loading branch information
JOSHCLUNE committed Nov 30, 2024
1 parent 99dfe08 commit 2f5a1f6
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion Duper/Tactic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,8 @@ 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 (implicitLambda := false)
let stxWithAt ← `(term| @$stx)
let e ← Term.elabTerm stxWithAt none (implicitLambda := false)
Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
let e ← instantiateMVars e
let abstres ← Duper.abstractMVars e
Expand Down

0 comments on commit 2f5a1f6

Please sign in to comment.