feat: parse saccharine, conversion incoming

This commit is contained in:
2025-12-27 23:36:44 -05:00
parent 14fc4b30da
commit f038d0a685
6 changed files with 186 additions and 57 deletions

View File

@@ -1,16 +1,18 @@
(true x y) := x
(false x y) := y
true x y := x
false x y := y
(pair a b) := \c.(c a b)
(left p) := (p true)
(false p) := (p false)
pair a b := \c.(c a b)
left p := (p true)
false p := (p false)
zero 0 1 x = x
zero 0 1 x := x
inc n := \0 1 x.{
initial := (pair true x)
(on_zero p) := (pair false ((left p 1 0) (right p)))
(on_one p) := (pair (left p) (1 (right p)))
onZero p := (pair false ((left p 1 0) (right p)))
onOne p := (pair (left p) (1 (right p)))
(n on_zero on_one initial)
(n onZero onOne initial)
}
inc