Changes
2 changed files (+22/-14)
-
-
@@ -529,10 +529,11 @@ | zero => "(16n)"| succ => "(17n)" | nat_rec => "(18n)" | unit => "(19n)" | intro => "(20n)" | ⊥ => "(21n)" | fls_rec => "(22n)" | name s => s!"(23n {s})" | unit_rec => "(20n)" | intro => "(21n)" | ⊥ => "(22n)" | fls_rec => "(23n)" | name s => s!"(24n {s})" | _ => panic "You should call dbify before using toString!" /-- Serialize a term-type pair -/
-
@@ -540,7 +541,7 @@ def serialize (p : Term × Term) :=s!"'({dbify [] p.1 |>.toString} . {dbify [] p.2 |>.toString})" -- Hardcode this into external proof checkers -- #eval toString <$> dbtypes -- #eval IO.FS.writeFile "dbtypes" <| "\n".intercalate <| toString <$> dbtypes |>.toList /- ## Proving some stuff
-
-
-
@@ -1,9 +1,16 @@["(4n (3n 0) (4n (4n (0n 0) (3n 0)) (4n (0n 1) (4n (2n (0n 1) (4n (0n 2) (3n 0)) (0n 0)) (5n (0n 3) (0n 2))))))", "(4n (3n 0) (4n (4n (0n 0) (3n 0)) (4n (4n (5n (0n 1) (0n 0)) (3n 0)) (4n (4n (0n 2) (4n (2n (0n 2) (4n (0n 3) (3n 0)) (0n 0)) (2n (0n 2) (4n (5n (0n 4) (0n 3)) (3n 0)) (2n (2n (2n (2n (6n) (4n (3n 0) (4n (4n (0n 0) (3n 0)) (4n (0n 1) (4n (2n (0n 1) (4n (0n 2) (3n 0)) (0n 0)) (5n (0n 3) (0n 2)))))) (0n 4)) (4n (4n (0n 4) (3n 0)) (4n (0n 5) (4n (2n (0n 1) (4n (0n 6) (3n 0)) (0n 0)) (5n (0n 7) (0n 2))))) (0n 3)) (4n (0n 4) (4n (2n (0n 4) (4n (0n 5) (3n 0)) (0n 0)) (5n (0n 6) (0n 5)))) (0n 1)) (4n (2n (0n 3) (4n (0n 4) (3n 0)) (0n 1)) (5n (0n 5) (0n 4))) (0n 0))))) (4n (5n (0n 3) (0n 2)) (2n (0n 2) (4n (5n (0n 4) (0n 3)) (3n 0)) (0n 0)))))))", "(4n (3n 0) (4n (3n 0) (4n (0n 1) (8n (0n 2) (0n 1)))))", "(4n (3n 0) (4n (3n 0) (4n (0n 0) (8n (0n 2) (0n 1)))))", "(4n (3n 0) (4n (3n 0) (4n (4n (8n (0n 1) (0n 0)) (3n 0)) (4n (4n (0n 2) (2n (0n 1) (4n (8n (0n 3) (0n 2)) (3n 0)) (2n (2n (2n (9n) (4n (3n 0) (4n (3n 0) (4n (0n 1) (8n (0n 2) (0n 1))))) (0n 3)) (4n (3n 0) (4n (0n 4) (8n (0n 5) (0n 1)))) (0n 2)) (4n (0n 3) (8n (0n 4) (0n 3))) (0n 0)))) (4n (4n (0n 2) (2n (0n 2) (4n (8n (0n 4) (0n 3)) (3n 0)) (2n (2n (2n (10n) (4n (3n 0) (4n (3n 0) (4n (0n 0) (8n (0n 2) (0n 1))))) (0n 4)) (4n (3n 0) (4n (0n 0) (8n (0n 6) (0n 1)))) (0n 3)) (4n (0n 3) (8n (0n 5) (0n 4))) (0n 0)))) (4n (8n (0n 4) (0n 3)) (2n (0n 3) (4n (8n (0n 5) (0n 4)) (3n 0)) (0n 0))))))))", "(4n (3n 0) (4n (0n 0) (12n (0n 0) (0n 0) (0n 1))))", "(4n (3n 0) (4n (0n 0) (4n (4n (0n 1) (4n (12n (0n 1) (0n 0) (0n 2)) (3n 0))) (4n (2n (2n (0n 0) (4n (0n 2) (4n (12n (0n 2) (0n 0) (0n 3)) (3n 0))) (0n 1)) (4n (12n (0n 1) (0n 1) (0n 2)) (3n 0)) (2n (2n (13n) (4n (3n 0) (4n (0n 0) (12n (0n 0) (0n 0) (0n 1)))) (0n 2)) (4n (0n 2) (12n (0n 0) (0n 0) (0n 3))) (0n 1))) (4n (0n 3) (4n (12n (0n 3) (0n 0) (0n 4)) (2n (2n (0n 3) (4n (0n 5) (4n (12n (0n 5) (0n 0) (0n 6)) (3n 0))) (0n 1)) (4n (12n (0n 4) (0n 1) (0n 5)) (3n 0)) (0n 0))))))))", "(3n 0)", "(15n)", "(4n (15n) (15n))", "(4n (4n (15n) (3n 1)) (4n (2n (0n 0) (4n (15n) (3n 1)) (16n)) (4n (4n (15n) (4n (2n (0n 2) (4n (15n) (3n 1)) (0n 0)) (2n (0n 3) (4n (15n) (3n 1)) (2n (17n) (4n (15n) (15n)) (0n 1))))) (4n (15n) (2n (0n 3) (4n (15n) (3n 1)) (0n 0))))))", "(3n 0)", "(19n)", "(3n 0)", "(4n (4n (21n) (3n 0)) (4n (21n) (2n (0n 1) (4n (21n) (3n 0)) (0n 0))))"] (4n (3n 0) (4n (4n (0n 0) (3n 0)) (4n (0n 1) (4n (2n (0n 1) (4n (0n 2) (3n 0)) (0n 0)) (5n (0n 3) (0n 2)))))) (4n (3n 0) (4n (4n (0n 0) (3n 0)) (4n (4n (5n (0n 1) (0n 0)) (3n 0)) (4n (4n (0n 2) (4n (2n (0n 2) (4n (0n 3) (3n 0)) (0n 0)) (2n (0n 2) (4n (5n (0n 4) (0n 3)) (3n 0)) (2n (2n (2n (2n (6n) (4n (3n 0) (4n (4n (0n 0) (3n 0)) (4n (0n 1) (4n (2n (0n 1) (4n (0n 2) (3n 0)) (0n 0)) (5n (0n 3) (0n 2)))))) (0n 4)) (4n (4n (0n 4) (3n 0)) (4n (0n 5) (4n (2n (0n 1) (4n (0n 6) (3n 0)) (0n 0)) (5n (0n 7) (0n 2))))) (0n 3)) (4n (0n 4) (4n (2n (0n 4) (4n (0n 5) (3n 0)) (0n 0)) (5n (0n 6) (0n 5)))) (0n 1)) (4n (2n (0n 3) (4n (0n 4) (3n 0)) (0n 1)) (5n (0n 5) (0n 4))) (0n 0))))) (4n (5n (0n 3) (0n 2)) (2n (0n 2) (4n (5n (0n 4) (0n 3)) (3n 0)) (0n 0))))))) (4n (3n 0) (4n (3n 0) (4n (0n 1) (8n (0n 2) (0n 1))))) (4n (3n 0) (4n (3n 0) (4n (0n 0) (8n (0n 2) (0n 1))))) (4n (3n 0) (4n (3n 0) (4n (4n (8n (0n 1) (0n 0)) (3n 0)) (4n (4n (0n 2) (2n (0n 1) (4n (8n (0n 3) (0n 2)) (3n 0)) (2n (2n (2n (9n) (4n (3n 0) (4n (3n 0) (4n (0n 1) (8n (0n 2) (0n 1))))) (0n 3)) (4n (3n 0) (4n (0n 4) (8n (0n 5) (0n 1)))) (0n 2)) (4n (0n 3) (8n (0n 4) (0n 3))) (0n 0)))) (4n (4n (0n 2) (2n (0n 2) (4n (8n (0n 4) (0n 3)) (3n 0)) (2n (2n (2n (10n) (4n (3n 0) (4n (3n 0) (4n (0n 0) (8n (0n 2) (0n 1))))) (0n 4)) (4n (3n 0) (4n (0n 0) (8n (0n 6) (0n 1)))) (0n 3)) (4n (0n 3) (8n (0n 5) (0n 4))) (0n 0)))) (4n (8n (0n 4) (0n 3)) (2n (0n 3) (4n (8n (0n 5) (0n 4)) (3n 0)) (0n 0)))))))) (4n (3n 1) (4n (0n 0) (12n (0n 0) (0n 0) (0n 1)))) (4n (3n 1) (4n (0n 0) (4n (4n (0n 1) (4n (12n (0n 1) (0n 0) (0n 2)) (3n 0))) (4n (2n (2n (0n 0) (4n (0n 2) (4n (12n (0n 2) (0n 0) (0n 3)) (3n 0))) (0n 1)) (4n (12n (0n 1) (0n 1) (0n 2)) (3n 0)) (2n (2n (13n) (4n (3n 1) (4n (0n 0) (12n (0n 0) (0n 0) (0n 1)))) (0n 2)) (4n (0n 2) (12n (0n 0) (0n 0) (0n 3))) (0n 1))) (4n (0n 3) (4n (12n (0n 3) (0n 0) (0n 4)) (2n (2n (0n 3) (4n (0n 5) (4n (12n (0n 5) (0n 0) (0n 6)) (3n 0))) (0n 1)) (4n (12n (0n 4) (0n 1) (0n 5)) (3n 0)) (0n 0)))))))) (3n 0) (15n) (4n (15n) (15n)) (4n (4n (15n) (3n 1)) (4n (2n (0n 0) (4n (15n) (3n 1)) (16n)) (4n (4n (15n) (4n (2n (0n 2) (4n (15n) (3n 1)) (0n 0)) (2n (0n 3) (4n (15n) (3n 1)) (2n (17n) (4n (15n) (15n)) (0n 1))))) (4n (15n) (2n (0n 3) (4n (15n) (3n 1)) (0n 0)))))) (3n 0) (19n) (4n (4n (19n) (3n 0)) (4n (2n (0n 0) (4n (19n) (3n 0)) (21n)) (4n (19n) (2n (0n 2) (4n (19n) (3n 0)) (0n 0))))) (3n 0) (4n (4n (22n) (3n 0)) (4n (22n) (2n (0n 1) (4n (22n) (3n 0)) (0n 0))))
-