From 2937675044bcefe266a9c1d1116dbec53ee3942a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 5 May 2024 13:25:48 -0700 Subject: [PATCH] feat: Library interface for calling no_confuse --- Pantograph/Goal.lean | 2 +- Pantograph/Library.lean | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 7ada190..11e5b20 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -521,7 +521,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu | .ok syn => pure syn | .error error => return .parseError error state.execute goalId (tacticM := Tactic.motivatedApply recursor) -protected def GoalState.tryNoConfusion (state: GoalState) (goalId: Nat) (eq: String): +protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Elab.TermElabM TacticResult := do state.restoreElabM let goal ← match state.savedState.tactic.goals.get? goalId with diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 00b4bc7..608aeeb 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -208,5 +208,8 @@ def goalFocus (state: GoalState) (goalId: Nat): Option GoalState := @[export pantograph_goal_motivated_apply_m] def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult := runTermElabM <| state.tryMotivatedApply goalId recursor +@[export pantograph_goal_no_confuse_m] +def goalNoConfuse (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult := + runTermElabM <| state.tryNoConfuse goalId recursor end Pantograph