uAgda-1.0.0.0: tutorial/02-Holes.ua

-- Module parametrization, universes, holes.
-----------------------------------------------

-- If you want to parameterize your module (think ML functors), just
-- use top-level abstraction: 

\ (Z : *) (plus : Z -> Z -> Z) -> ( 

-- Note that parentheses are needed here (check operator precedence in
-- the source code: "RawSyntax.hs" contains the syntax in BNF)


-- We define Leibniz equality for good measure:
Eq = \ A a b -> (P : A -> *) -> P a -> P b
     : (A : *) -> (a b : A) -> *1,

-- By default uAgda is predicative, hence Leibniz equality is in 
-- *1.

-- Sometimes you may want to omit the definition for a particular
-- term. (For example you know a theorem to hold but you'd rather
-- write the proof later.)  In that case you can use the "hole"
-- construct as follows. 

plus-commutative = \ (x : Z) (y : Z) -> (?x : Eq Z (plus x y) (plus y x)),

-- Note that uAgda shows the context of the hole, so it's easier to
-- fill it in later.

-- End of tuple.
*)