aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

chore: Version 0.3 #136

Open
aniva wants to merge 487 commits from dev into main
pull from: dev
merge into: aniva:main
Conversation 0 Commits 487 Files Changed 52 +5
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 111781816f - Show all commits

5
Test/Proofs.lean
View File

@ -232,6 +232,11 @@ def proof_or_comm: TestM Unit := do
addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
let state2parent ← serialize_expression_ast state2.parentExpr?.get! (sanitize := false)
-- This is due to delayed assignment
addTest $ LSpec.test "(2 parent)" (state2parent ==
"((:mv _uniq.45) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with
| .success state => pure state | .success state => pure state
| other => do | other => do