-- Modules, type annotations, Sigma
-------------------------------------

-- Usually you will want to break down your definitions
-- into multiple parts. That can be done by making the
-- top-level term a tuple. 

-- For example, this file starts with:
Nat = (N : *) -> (N -> N) -> N -> N,

-- which declares the 1st component of the tuple, and gives
-- it a name.


-- Let's define some more stuff:
zer = \N s z -> z : Nat,


-- Note that every term may be annotated by its type.  This is good
-- because no type inference is done.  (Even though the system is
-- clever enough to push down type annotations in lambdas)

-- Let's define the standard Church numeral toolbox:


suc = \m N s z -> s (m N s z) 
    : Nat -> Nat,

plus = \n m N s z -> n N s (m N s z)
     : Nat -> Nat -> Nat,

mul = \n m N s -> n N (m N s)
    : Nat -> Nat -> Nat,

exp = \n m N -> m (N -> N) (n N)
    : Nat -> Nat -> Nat,


-- Now we're ready for some calculation! (the results can be seen in
-- the normal form)
one = suc zer,
two = suc one,
four = exp two (mul two two),

-- The syntax for pairs is "first class", we can have them anywhere:
somePair = (pi1 = two, plus two four) : (Nat ;; Nat),


-- Dependent pairs can also be declared
depPair  = (A = Nat, suc) : ((A : *1) ;; A -> A),

-- fields named in the type can be extracted using .:
extract = depPair.A,

-- Finally we must give the last component of the tuple, which is NOT
-- named.  Since we have nothing special in mind, let's just give a
-- random simple term:

*