chore: Version 0.3 #136
|
@ -200,7 +200,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
||||||
goalStates := state.goalStates.insert nextStateId nextGoalState,
|
goalStates := state.goalStates.insert nextStateId nextGoalState,
|
||||||
nextId := state.nextId + 1
|
nextId := state.nextId + 1
|
||||||
}
|
}
|
||||||
let goals ← nextGoalState.serializeGoals (parent := .some target) (options := state.options)
|
let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options)
|
||||||
return .ok {
|
return .ok {
|
||||||
nextStateId? := .some nextStateId,
|
nextStateId? := .some nextStateId,
|
||||||
goals? := .some goals,
|
goals? := .some goals,
|
||||||
|
|
Loading…
Reference in New Issue