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
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66

; Get second element of list (0-indexed)
!(def arg1 (lambda (x) (car (cdr x))))

; Get left element of tuple at second position in list
!(def arg1a (lambda (x) (car (arg1 x))))

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

; Get third element of list
!(def arg2 (lambda (x) (car (cdr (cdr x)))))

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

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

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

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

; NEED defrec instead of def for recursive functions
; TODO: Implement nats
!(defrec check (lambda (env typ term)
  (if (eq (car term) "var")
    (eq typ (eval (arg1 term) env))
  (if (and (eq (car typ) "fn") (eq (car term) "lam"))
    (and (eq (arg2 typ) (arg2a term))
      ; Crazy eval magic
      (check (eval (list 'let (list (list (arg1 term) (list 'quote (arg1 typ)))) '(current-env)) env) (arg2a term) (arg2b term)))
  (if (and (eq (car term) "app") (eq (car (arg1a term)) "fn"))
    (and (eq (arg1 (arg1a term)) (arg2a term)) (and (eq (arg2 (arg1a term)) typ)
      (and (check env (arg1a term) (arg1b term))
        (check env (arg2a term) (arg2b term)))))
  (if (and (eq (car typ) "prod") (eq (car term) "and"))
    (and (eq (arg1a term) (arg1 typ)) (and (eq (arg2a term) (arg2 typ))
      (and (check env (arg1a term) (arg1b term)) (check env (arg2a term) (arg2b term)))))
  (if (and (eq (car term) "and1") (eq (car (arg1a term)) "prod"))
    (and (eq (arg1 (arg1a term)) typ)
      (check env (arg1a term) (arg1b term)))
  (if (and (eq (car term) "and2") (eq (car (arg1a term)) "prod"))
    (and (eq (arg2 (arg1a term)) typ)
      (check env (arg1a term) (arg1b term)))
  (if (and (eq (car typ) "sum") (eq (car term) "or"))
    (and (or (eq (arg1a term) (arg1 typ)) (eq (arg1a term) (arg2 typ)))
      (check env (arg1a term) (arg1b term)))
  (if (and (eq (car term) "fls_elim") (eq (car (arg1a term))))
    t
  nil))))))))))

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

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

!(def a_imp_b_imp_ba (cons (list "fn" (list "new" "A") (list "fn" (list "new" "B") (list "prod" (list "new" "B") (list "new" "A")))) (list "lam" 'a (cons (list "fn" (list "new" "B") (list "prod" (list "new" "B") (list "new" "A"))) (list "lam" 'b (cons (list "prod" (list "new" "B") (list "new" "A")) (list "and" (cons (list "new" "B") (list "var" 'b)) (cons (list "new" "A") (list "var" 'a)))))))))

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

!(def ab_imp_ba (cons (list "fn" (list "prod" (list "new" "A") (list "new" "B")) (list "prod" (list "new" "B") (list "new" "A"))) (list "lam" 'ab (cons (list "prod" (list "new" "B") (list "new" "A")) (list "and" (cons (list "new" "B") (list "and2" (cons (list "prod" (list "new" "A") (list "new" "B")) (list "var" 'ab)))) (cons (list "new" "A") (list "and1" (cons (list "prod" (list "new" "A") (list "new" "B")) (list "var" 'ab)))))))))

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

!(def not_ab_imp_not_a (cons (list "fn" (list "fn" (list "sum" (list "new" "A") (list "new" "B")) '("fls")) (list "fn" (list "new" "A") '("fls"))) (list "lam" 'f (cons (list "fn" (list "new" "A") '("fls")) (list "lam" 'x (cons '("fls") (list "app" (cons (list "fn" (list "sum" (list "new" "A") (list "new" "B")) '("fls")) (list "var" 'f)) (cons (list "sum" (list "new" "A") (list "new" "B")) (list "or" (cons (list "new" "A") (list "var" 'x)))))))))))

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