From 267290c8f71a83309ef217c53b8c44de293692ea Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 23 Feb 2025 14:14:59 -0800 Subject: [PATCH] fix: Draft tactic failure by new `sorry` semantics --- Pantograph/Tactic/Assign.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Pantograph/Tactic/Assign.lean b/Pantograph/Tactic/Assign.lean index c87dd46..af9d15f 100644 --- a/Pantograph/Tactic/Assign.lean +++ b/Pantograph/Tactic/Assign.lean @@ -28,15 +28,16 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do Elab.Tactic.replaceMainGoal nextGoals def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := do - Meta.transform src λ - | .app (.app (.const ``sorryAx ..) type) .. => do - let type ← instantiateMVars type + Meta.transform src λ expr => + if expr.isSorry then do + let type ← instantiateMVars (expr.getArg! 0 |>.bindingBody!) if type.hasSorry then throwError s!"Coupling is not allowed in draft tactic: {← Meta.ppExpr type}" let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type modify (mvar.mvarId! :: .) pure $ .done mvar - | _ => pure .continue + else + pure .continue -- Given a complete (no holes) expression, extract the sorry's from it and convert them into goals. def draft (goal : MVarId) (expr : Expr) : MetaM (List MVarId) := do