Merge branch 'dev' into misc/toolchain
This commit is contained in:
commit
a4a1dfabef
|
@ -225,6 +225,10 @@ protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
|
|||
let expr := goalState.mctx.eAssignment.find! parent
|
||||
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
|
||||
return expr
|
||||
protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do
|
||||
let expr ← goalState.mctx.eAssignment.find? mvar
|
||||
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
|
||||
return expr
|
||||
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -243,7 +243,7 @@ structure GoalPrintResult where
|
|||
-- The root expression
|
||||
root?: Option Expression := .none
|
||||
-- The filling expression of the parent goal
|
||||
parent?: Option Expression := .none
|
||||
parent?: Option Expression
|
||||
deriving Lean.ToJson
|
||||
|
||||
-- Diagnostic Options, not available in REPL
|
||||
|
|
|
@ -97,6 +97,12 @@ def test_tactic : IO LSpec.TestSeq :=
|
|||
goals? := #[goal1],
|
||||
}:
|
||||
Protocol.GoalTacticResult)),
|
||||
subroutine_step "goal.print"
|
||||
[("stateId", .num 1)]
|
||||
(Lean.toJson ({
|
||||
parent? := .some { pp? := .some "fun x => ?m.11 x" },
|
||||
}:
|
||||
Protocol.GoalPrintResult)),
|
||||
subroutine_step "goal.tactic"
|
||||
[("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
|
||||
(Lean.toJson ({
|
||||
|
|
Loading…
Reference in New Issue