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
  | .A fn arg =>
    match red fn with
    | .L body => let rec sub : Nat → Term → Term
      | n, (.A fn arg) => .A (sub n fn) (sub n arg)
      | n, (.L body) => .L (sub (n + 1) body)
      | n, (.V n') => if n == n' then arg else .V n'
      sub 0 body
    | other => .A other arg
  | other => other

#eval red <| .A (.L (.V 69)) (.V 1)