feat: fun little program

This commit is contained in:
2025-12-28 00:53:43 -05:00
parent f4897d53a9
commit 4d81aca0b2
4 changed files with 56 additions and 15 deletions

View File

@@ -1,19 +1,52 @@
true x y := x
false x y := y
T x y := x
F x y := y
if b t e := (b t e)
pair a b := \c.(c a b)
left p := (p true)
false p := (p false)
left p := (p T)
right p := (p F)
zero 0 1 x := x
print n := (n 0 1 end)
inc n := \0 1 x.{
initial := (pair true x)
onZero p := (pair false ((left p 1 0) (right p)))
onOne p := (pair (left p) (1 (right p)))
(n onZero onOne initial)
}
fix f := (\x.(f (x x)) \x.(f (x x)))
(print zero)
some x := (pair T x)
none := \.F
isfull := left
unwrap := right
nil := none
push i l := (some (pair i l))
peek l := (left (unwrap l))
pop l := (right (unwrap l))
inc := (fix \self l.{
(if (isfull l)
(if (peek l)
(push F (self (pop l)))
(push T (pop l))
)
(push T nil)
)
})
print := (fix \self l.{
(if (isfull l)
((if (peek l) 1 0) (self (pop l)))
END
)
})
one := (push T nil)
double N := (push F N)
N :=
(double (double (double (double (double
(double (double (double (double (double
(double (double (double (double (double
(double (double (double (double (double
(double (double (double (double (double
(double (double (double (double (double
one))))))))))))))))))))))))))))))
(print N)