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
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27

!(def arg1 (lambda (x) (car (cdr x))))

!(def arg2 (lambda (x) (car (cdr (cdr x)))))

!(def arg21 (lambda (x) (car (arg2 x))))

!(def arg22 (lambda (x) (cdr (arg2 x))))

; Boolean and
!(def and (lambda (x y) (if x (if y t nil) nil)))

; NEED defrec instead of def for recursive functions
!(defrec check (lambda (env typ term)
  (if (eq (car term) "var")
    (eq typ (eval (cdr term) env))
  (if (and (eq (car typ) "fn") (eq (car term) "lam"))
    (and (eq (arg2 typ) (arg21 term)) (check (eval (list 'let (list (list (arg1 term) (list 'quote (arg1 typ)))) '(current-env)) env) (arg21 term) (arg22 term)))
  nil))))

; Autogenerated by Main.lean
!(def a_imp_a (cons (list "fn" (cons "new" "A") (cons "new" "A")) (list "lam" 'a (cons (cons "new" "A") (cons "var" 'a)))))

(check (empty-env) (car a_imp_a) (cdr a_imp_a))

; !(def env (empty-env))
; !(def typ (car a_imp_a))
; !(def term (cdr a_imp_a))