aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

fix: Consistent naming in library functions

This commit is contained in:
Leni Aniva 2024-05-08 20:51:36 -07:00
parent 66a5dfcf3c
commit e58dbc66a9
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 3 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
Pantograph/Library.lean
View File

@ -180,6 +180,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
parent? := ← state.parentExpr?.mapM (λ expr => do parent? := ← state.parentExpr?.mapM (λ expr => do
serializeExpression options (← unfoldAuxLemmas expr)), 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] @[export pantograph_goal_tactic_m]
def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := 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 := def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.CoreM TacticResult :=
runTermElabM <| state.tryNoConfuse goalId eq 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 end Pantograph