define 1, +, =, and 2, and also how these are composed (are these prefix operators, postfix operators, infix operators)
because this clearly doesn't work
because this clearly doesn't work
1 + 1 = 2
+ 1 = 2
\x. 1 2 (= 2 x)
\x. 2 (= 2 x)
\x. \y. = 2 x (= 2 x y)
\x. \y. and (LEQ 2 x) (LEQ x 2) (= 2 x y)
\x. \y. LEQ 2 x (LEQ x 2) (LEQ 2 x) (= 2 x y)
\x. \y. IsZero (minus 2 x) (LEQ x 2) (LEQ 2 x) (= 2 x y)
\x. \y. minus 2 x (\z. false) true (LEQ x 2) (LEQ 2 x) (= 2 x y)
\x. \y. x pred 2 (\z. false) true (LEQ x 2) (LEQ 2 x) (= 2 x y)
\x. \y. x pred 2 (\z. false) true (IsZero (minus x 2)) (LEQ 2 x) (= 2 x y)
\x. \y. x pred 2 (\z. false) true (minus x 2 (\z. false) true) (LEQ 2 x) (= 2 x y)
\x. \y. x pred 2 (\z. false) true (2 pred x (\z. false) true) (LEQ 2 x) (= 2 x y)
\x. \y. x pred 2 (\z. false) true (pred (pred x) (\z. false) true) (LEQ 2 x) (= 2 x y)
\x. \y. x pred 2 (\z. false) true (pred x (\g. \h. h (g (\z. false))) (\u. true) (\u. u)) (LEQ 2 x) (= 2 x y)
[The lambda expressions that follow have been considered universally useless for human viewing. The previous one was the final one that had any use to anyone.]
Comments
There are no comments here yet!
Come back later to see if someone commented something or create one!