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

import Std.Data.HashMap

inductive Typ
  | var : String → Typ
  | fn : Typ → Typ → Typ
  | prod : Typ → Typ → Typ
  | sum : Typ → Typ → Typ
deriving BEq

inductive Term
  | var : Typ → String → Term
  | fn : Typ → String → Term → Term
  | app : Typ → Term → Term → Term
  | prod : Typ → Term → Term → Term
  | sum : Typ → Term → Term → Term

def Term.getTyp : Term → Typ
  | .var τ _ => τ
  | .fn τ _ _ => τ
  | .app τ _ _ => τ
  | .prod τ _ _ => τ
  | .sum τ _ _ => τ

def check (env : Std.HashMap String Typ) : Term → Bool
  | .var τ x =>
    (· == τ) <$> env[x]? |>.getD false
  | .fn τ x b =>
    match τ with
    | .fn α β => b.getTyp == β && check (env.insert x α) b
    | _ => false
  | .app τ f x =>
    match f.getTyp with
    | .fn α β => x.getTyp == α && β == τ && check env f && check env x
    | _ => false
  | .prod τ x y =>
    match τ with
    | .prod α β =>
      x.getTyp == α && y.getTyp == β && check env x && check env y
    | _ => false
  | .sum τ x y =>
    match τ with
    | .sum α β =>
      x.getTyp == α && y.getTyp == β && check env x && check env y
    | _ => false

def ab_imp_ba := Term.fn (.fn (.var "A") (.fn (.var "B") (.prod (.var "B") (.var "A")))) "a" (.fn (.fn (.var "B") (.prod (.var "B") (.var "A"))) "b" (.prod (.prod (.var "B") (.var "A")) (.var (.var "B") "b") (.var (.var "A") "a")))

#eval check (.ofList []) ab_imp_ba