1  module Main where
 2  
 3  import Core
 4  
 5  -- import Parse
 6  
 7  main :: IO ()
 8  main = pure ()
 9  
10  -- let Nat  : * = forall N:*. (N -> N) -> (N -> N);
11  -- let add  : Nat -> Nat -> Nat = \a b N s z. a N s (b N s z);
12  church_add :: Term
13  church_add =
14    let
15      n_to_n = Pi (Var 1) (Var 1)
16      nton_to_nton = Pi n_to_n n_to_n
17      church_nat = Pi (U 0) nton_to_nton
18    in
19      Let 0 (U 0) church_nat $
20        Let
21          0
22          ( Pi
23              (Pi (Var 1) (Var 2))
24              (Var 1)
25          )
26          ( Lam $
27              Lam $
28                Lam $
29                  Lam $
30                    Lam $
31                      (Var 4)
32                        `App` (Var 2)
33                        `App` (Var 1)
34                        `App` ((Var 3) `App` (Var 2) `App` (Var 1) `App` (Var 0))
35          )
36          (Var 0)