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

test(tactic): Check fragments have been erased

This commit is contained in:
Leni Aniva 2025-07-07 14:47:50 -07:00
parent 2dbbe2509e
commit 92befda2ff
Signed by: aniva
GPG Key ID: D5F96287843E8DFB
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Test/Tactic/Fragment.lean
View File

@ -126,8 +126,8 @@ def test_conv_simple: TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.check tactic ((← stateF.serializeGoals).map (·.devolatilize) = checkEq tactic ((← stateF.serializeGoals).map (·.devolatilize)) #[]
#[]) checkEq "fragments" stateF.fragments.size 0
where where
h := "b + a + c1 = b + a + c2" h := "b + a + c1 = b + a + c2"
@ -180,6 +180,7 @@ def test_conv_unshielded : TestM Unit := do
let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed" let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
let root? := state.rootExpr? let root? := state.rootExpr?
checkTrue "root" root?.isSome checkTrue "root" root?.isSome
checkEq "fragments" state.fragments.size 0
where where
interiorGoal (free: List (String × String)) (target: String) := interiorGoal (free: List (String × String)) (target: String) :=
let free := [("p", "Prop"), ("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("hp", "p"), ("hi", "p → x = y")] ++ free let free := [("p", "Prop"), ("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("hp", "p"), ("hi", "p → x = y")] ++ free