example/lambda/example.lambda

   1 def id = \x.x
   2 def true = \t.\f.t
   3 def false = \t.\f.f
   4 def test = \l.\m.\n.((l m) n)
   5 def and = \b.\c.((b c) false)
   6 def or = \b.\c.((b true) c)
   7 def not = \b.((b false) true)
   8 def pair = \f.\s.\b.((b f) s)
   9 def fst = \p.(p true)
  10 def snd = \p.(p false)
  11 def c0 = \s.\z.z
  12 def c1 = \s.\z.(s z)
  13 def c2 = \s.\z.(s (s z))
  14 def c3 = \s.\z.(s (s (s z)))
  15 def c4 = \s.\z.(s (s (s (s z))))
  16 def c5 = \s.\z.(s (s (s (s (s z)))))
  17 def succ = \n.\s.\z.(s ((n s) z))
  18 def plus = \m.\n.\s.\z.((m s) ((n s) z))
  19 def times = \m.\n.((m (plus n)) c0)
  20 def power = \m.\n.(m n)
  21 def is_zero = \m.((m \x.false) true)
  22 def zz = ((pair c0) c0)
  23 def ss = \p.((pair (snd p)) ((plus c1) (snd p)))
  24 def pred = \m.(fst ((m ss) zz))
  25 def minus = \m.\n.((n pred) m)
  26 def equal = \m.\n.((and (is_zero ((m pred) n))) (is_zero ((n pred) m)))
  27
  28 ((equal ((minus ((times c4) c4)) ((power c2) c4))) c0)