-- 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: *