Simple lambda calculus interpreter

Changes

1 changed files (+20/-0)

• lambcalc.lean (new)
  • @@ -0,0 +1,20 @@
    + -- Simple lambda calculus interpreter using de Bruijin indices + -- https://jameshfisher.com/2018/03/15/a-lambda-calculus-interpreter-in-haskell/ + + inductive Term where + | A : Term → Term → Term + | L : Term → Term + | V : Nat → Term + + def red : Term → Term + | Term.A fn arg => + match red fn with + | Term.L body => let rec sub : Nat → Term → Term + | n, (Term.A fn arg) => Term.A (sub n fn) (sub n arg) + | n, (Term.L body) => Term.L (sub (n + 1) body) + | n, (Term.V n') => if n == n' then arg else Term.V n' + sub 0 body + | other => Term.A other arg + | other => other + + #eval red <| Term.A (Term.L (Term.V 69)) (Term.V 1)