ecc http://http://www.openmath.org/cd/ecc.ocd 2000-09-01 experimental 1999-09-07 1 1 relation1 Extended Calculus of Constructions Primitives Initial version: O. Caprotti (July 1, 1999) Revised: O. Caprotti (September 8, 1999) type Attribution tag to denote type-judgement typecoerce Attribution tag to denote type-judgement with coercion SigmaType The binder symbol used to construct the type of Cartesian products. The (either plain or attributed) variables might occur in the body \OM\ object. Pair The pairing constructor. It takes two OpenMath objects as first element and second element of the pair, and a third optional OpenMath object that represents the type of the pair. 0 1 PairProj1 The first projection function that extracts the first component of a Pair. It satisfies the sigma-reduction rule. 0 1 0 PairProj2 The second projection function that extracts the second component of a Pair. It satisfies sigma-reduction rule. 0 1 1 Tuple The n-ary tupling constructor when n>2. The arguments are the element of the tuple. Tuple objects can also be constructed by successive nesting of Pair. 0 1 2 0 1 2