Next: LESS Up: The Rules Previous: VOID

INT

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

* formation universe_intro_integer: rule.

int_equality: rule.

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

* canonical integer_intro_integer(c): int

rule.

integer_equality_natural_number: rule.

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

* noncanonical integer_equality_minus: rule.

integer_intro_addition: rule.

integer_intro_subtraction: rule.

integer_intro_multiplication: rule.

integer_intro_division: rule.

integer_intro_modulo: rule.

integer_equality_addition: rule.

integer_equality_subtraction: rule.

integer_equality_multiplication: rule.

integer_equality_division: rule.

integer_equality_modulo: rule.

integer_elim(hyp y z): int tok tok rule.

integer_equality_induction(over_id over u v): tok term tok tok rule.

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

* equality int_eq_equality: rule.

int_less_equality: rule.

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

* computation integer_computation(kind where): tok

int

rule.

where kind should be one of `UP`, `BASE` or `DOWN`.

int_eq_computation(where): int rule.

int_less_computation(where): int rule.

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