feat: Add support for the have, conv, and calc tactics #59

Merged
aniva merged 22 commits from goal/have-conv-calc into dev 2024-04-11 15:36:20 -07:00
1 changed files with 4 additions and 0 deletions
Showing only changes of commit 222cb035d1 - Show all commits

View File

@ -178,6 +178,10 @@ def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult :=
def goalConvExit (state: GoalState): Lean.CoreM TacticResult := def goalConvExit (state: GoalState): Lean.CoreM TacticResult :=
runTermElabM <| state.convExit runTermElabM <| state.convExit
@[export pantograph_goal_calc_m]
def goalCalc (state: GoalState) (goalId: Nat) (pred: String): Lean.CoreM TacticResult :=
runTermElabM <| state.tryCalc goalId pred
@[export pantograph_goal_focus] @[export pantograph_goal_focus]
def goalFocus (state: GoalState) (goalId: Nat): Option GoalState := def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
state.focus goalId state.focus goalId