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

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
Conversation 0 Commits 22 Files Changed 9 +11 -3
1 changed files with 11 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 9fbc65829d - Show all commits

14
Pantograph/Library.lean
View File

@ -162,15 +162,23 @@ def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
@[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 :=
runTermElabM <| GoalState.tryTactic state goalId tactic runTermElabM <| state.tryTactic goalId tactic
@[export pantograph_goal_assign_m] @[export pantograph_goal_assign_m]
def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult := def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult :=
runTermElabM <| GoalState.tryAssign state goalId expr runTermElabM <| state.tryAssign goalId expr
@[export pantograph_goal_have_m] @[export pantograph_goal_have_m]
def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult :=
runTermElabM <| GoalState.tryHave state goalId binderName type runTermElabM <| state.tryHave goalId binderName type
@[export pantograph_goal_conv_m]
def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult :=
runTermElabM <| state.conv goalId
@[export pantograph_goal_conv_exit_m]
def goalConvExit (state: GoalState): Lean.CoreM TacticResult :=
runTermElabM <| state.convExit
@[export pantograph_goal_continue] @[export pantograph_goal_continue]
def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState := def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=