next up previous contents index
Next: UNION Up: The Rules Previous: LESS

LIST

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

* formation universe_intro_list: rule.

list_equality(level): int rule.

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

* canonical list_intro_nil(level): int rule.

list_equality_nil(level): int rule.

list_intro_cons: rule.

list_equality_cons: rule.

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

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

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

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

* computation list_computation(where): int rule.


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