Next: FUNCTION Up: The Rules Previous: LIST

UNION

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

* formation universe_intro_union: rule.

union_equality: rule.

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

* canonical union_intro_left(level): int

rule.

union_equality_inl(level): int rule.

union_intro_right(level): int rule.

union_equality_inr(level): int rule.

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

* noncanonical union_elim(hyp x y): int

tok

rule.

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

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

* computation union_computation(where): int

rule.

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