1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 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)