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
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45

!(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)))

!(def 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)) (eval '(let (( (arg1 typ))) (check env (arg2 typ) (arg22 term)))) (env))
  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)))))

!(def typ (car a_imp_a))

!(def term (cdr a_imp_a))

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


; 123

; (+ 1 1)

; !(def square (lambda (x) (* x x)))

; (square 8)

; !(def make-adder
;    (lambda (n)
;      (lambda (x)
;        (+ x n))))

; !(def five-plus
;    (make-adder 5))

; (five-plus 3)