aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 14 Pull Requests 2 Packages Projects Releases Wiki Activity

test(repl): MVar name mismatch fix

This commit is contained in:
Leni Aniva 2025-07-02 15:02:35 -07:00
parent d1998b129a
commit 726c2ed145
Signed by: aniva
GPG Key ID: D5F96287843E8DFB
1 changed files with 8 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
Test/Integration.lean
View File

@ -168,15 +168,15 @@ def test_conv_calc : Test := do
step "options.set" ({automaticMode? := .some false}: Protocol.OptionsSet) step "options.set" ({automaticMode? := .some false}: Protocol.OptionsSet)
({}: Protocol.OptionsSetResult) ({}: Protocol.OptionsSetResult)
step "goal.start" ({ expr := "∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b"} : Protocol.GoalStart) step "goal.start" ({ expr := "∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b"} : Protocol.GoalStart)
({ stateId := 0, root := "_uniq.163" }: Protocol.GoalStartResult) ({ stateId := 0, root := "_uniq.171" }: Protocol.GoalStartResult)
let vars := #[ let vars := #[
{ name := "_uniq.164", userName := "a", type? := .some { pp? := .some "Nat" }}, { name := "_uniq.172", userName := "a", type? := .some { pp? := .some "Nat" }},
{ name := "_uniq.167", userName := "b", type? := .some { pp? := .some "Nat" }}, { name := "_uniq.175", userName := "b", type? := .some { pp? := .some "Nat" }},
{ name := "_uniq.170", userName := "h", type? := .some { pp? := .some "b = 2" }}, { name := "_uniq.178", userName := "h", type? := .some { pp? := .some "b = 2" }},
] ]
let goal : Protocol.Goal := { let goal : Protocol.Goal := {
vars, vars,
name := "_uniq.171", name := "_uniq.179",
target := { pp? := "1 + a + 1 = a + b" }, target := { pp? := "1 + a + 1 = a + b" },
} }
step "goal.tactic" ({ stateId := 0, tactic? := .some "intro a b h" }: Protocol.GoalTactic) step "goal.tactic" ({ stateId := 0, tactic? := .some "intro a b h" }: Protocol.GoalTactic)
@ -185,13 +185,13 @@ def test_conv_calc : Test := do
({ nextStateId? := .some 2, goals? := #[{ goal with fragment := .calc }], }: Protocol.GoalTacticResult) ({ nextStateId? := .some 2, goals? := #[{ goal with fragment := .calc }], }: Protocol.GoalTacticResult)
let goalCalc : Protocol.Goal := { let goalCalc : Protocol.Goal := {
vars, vars,
name := "_uniq.363", name := "_uniq.381",
userName? := .some "calc", userName? := .some "calc",
target := { pp? := "1 + a + 1 = a + 1 + 1" }, target := { pp? := "1 + a + 1 = a + 1 + 1" },
} }
let goalMain : Protocol.Goal := { let goalMain : Protocol.Goal := {
vars, vars,
name := "_uniq.382", name := "_uniq.400",
fragment := .calc, fragment := .calc,
target := { pp? := "a + 1 + 1 = a + b" }, target := { pp? := "a + 1 + 1 = a + b" },
} }
@ -201,7 +201,7 @@ def test_conv_calc : Test := do
goalCalc with goalCalc with
fragment := .conv, fragment := .conv,
userName? := .none, userName? := .none,
name := "_uniq.450", name := "_uniq.468",
} }
step "goal.tactic" ({ stateId := 3, mode? := .some "conv" }: Protocol.GoalTactic) step "goal.tactic" ({ stateId := 3, mode? := .some "conv" }: Protocol.GoalTactic)
({ nextStateId? := .some 4, goals? := #[goalConv], }: Protocol.GoalTacticResult) ({ nextStateId? := .some 4, goals? := #[goalConv], }: Protocol.GoalTacticResult)