feat: Add library bindings for calc
This commit is contained in:
parent
6b44d9ef14
commit
6d85c19589
|
@ -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
|
||||||
|
|
Loading…
Reference in New Issue