fix(goal): Unknown metavariable problem during fragment initialization #222
|
@ -132,8 +132,9 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExprs: Bool) (goals: Bo
|
||||||
pure .none
|
pure .none
|
||||||
let parentExprs? ← if parentExprs then
|
let parentExprs? ← if parentExprs then
|
||||||
.some <$> state.parentMVars.mapM λ parent => parent.withContext do
|
.some <$> state.parentMVars.mapM λ parent => parent.withContext do
|
||||||
let val := state.getMVarEAssignment parent |>.get!
|
let val? := state.getMVarEAssignment parent
|
||||||
serializeExpression options (← instantiateAll val)
|
val?.mapM λ val => do
|
||||||
|
serializeExpression options (← instantiateAll val)
|
||||||
else
|
else
|
||||||
pure .none
|
pure .none
|
||||||
let goals ← if goals then
|
let goals ← if goals then
|
||||||
|
|
|
@ -325,7 +325,7 @@ structure GoalPrintResult where
|
||||||
-- The root expression
|
-- The root expression
|
||||||
root?: Option Expression := .none
|
root?: Option Expression := .none
|
||||||
-- The filling expression of the parent goal
|
-- The filling expression of the parent goal
|
||||||
parentExprs?: Option (List Expression) := .none
|
parentExprs?: Option (List (Option Expression)) := .none
|
||||||
goals: Array Goal := #[]
|
goals: Array Goal := #[]
|
||||||
extraMVars: Array Expression := #[]
|
extraMVars: Array Expression := #[]
|
||||||
|
|
||||||
|
|
|
@ -91,7 +91,7 @@ def test_tactic : Test := do
|
||||||
step "goal.print" ({ stateId := 1, parentExprs? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
|
step "goal.print" ({ stateId := 1, parentExprs? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
|
||||||
({
|
({
|
||||||
root? := .some { pp? := "fun x => ?m.11"},
|
root? := .some { pp? := "fun x => ?m.11"},
|
||||||
parentExprs? := .some [{ pp? := .some "fun x => ?m.11" }],
|
parentExprs? := .some [.some { pp? := .some "fun x => ?m.11" }],
|
||||||
}: Protocol.GoalPrintResult)
|
}: Protocol.GoalPrintResult)
|
||||||
step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
|
step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
|
||||||
({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult)
|
({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult)
|
||||||
|
|
Loading…
Reference in New Issue