From e58dbc66a92ef10b014a30745a542ec0dd9be6ef Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 8 May 2024 20:51:36 -0700 Subject: [PATCH] fix: Consistent naming in library functions --- Pantograph/Library.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index fa5d414..3ae852f 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -180,6 +180,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto parent? := ← state.parentExpr?.mapM (λ expr => do serializeExpression options (← unfoldAuxLemmas expr)), } +@[export pantograph_goal_diag_m] +def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String := + runMetaM $ state.diag diagOptions @[export pantograph_goal_tactic_m] def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := @@ -212,8 +215,4 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.CoreM TacticResult := runTermElabM <| state.tryNoConfuse goalId eq -@[export pantograph_goal_diag] -def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String := - runMetaM $ state.diag diagOptions - end Pantograph