From 679871cbc659ce9ff58e832d20f51f52ae3dc2f1 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 5 May 2024 13:26:46 -0700 Subject: [PATCH] fix: NoConfuse arg name --- Pantograph/Library.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 608aeeb..6dda2f0 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -209,7 +209,7 @@ def goalFocus (state: GoalState) (goalId: Nat): Option GoalState := 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 +def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.CoreM TacticResult := + runTermElabM <| state.tryNoConfuse goalId eq end Pantograph