next up previous contents index
Next: QUOTIENT Up: The Rules Previous: FUNCTION

PRODUCT

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* formation universe_intro_product(x left_term): tok term rule.

product_equality(y): tok rule.

universe_intro_product_independent: rule.

product_equality_independent: rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* canonical product_intro_dependent(left_term level y): term int tok rule.

product_equality_pair(level y): int tok rule.

product_intro: rule.

product_equality_pair_independent: rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* noncanonical product_elim(hyp u v): int tok tok rule.

product_equality_spread(over_id over using u v): tok term term tok tok rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* computation product_computation(where): int rule.


Richard Eaton
Thu Sep 14 08:45:18 EDT 1995