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
2 changed files with 17 additions and 4 deletions
Showing only changes of commit 9a04fd4819 - Show all commits

View File

@ -327,6 +327,16 @@ protected def GoalState.convExit (state: GoalState):
protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
let goal ← state.savedState.tactic.goals.get? goalId
return {
state with
savedState := {
state.savedState with
tactic := { goals := [goal] },
},
}
/--
Brings into scope a list of goals
-/
@ -345,7 +355,6 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
tactic := { goals := unassigned },
},
}
/--
Brings into scope all goals from `branch`
-/

View File

@ -178,14 +178,18 @@ def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult :=
def goalConvExit (state: GoalState): Lean.CoreM TacticResult :=
runTermElabM <| state.convExit
@[export pantograph_goal_continue]
def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
target.continue branch
@[export pantograph_goal_focus]
def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
state.focus goalId
@[export pantograph_goal_resume]
def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
@[export pantograph_goal_continue]
def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
target.continue branch
@[export pantograph_goal_serialize_m]
def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
runMetaM <| state.serializeGoals (parent := .none) options