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

FUNCTION

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

* formation universe_intro_function(x term): tok term rule.

function_equality(y): tok rule.

universe_intro_function_independent: rule.

function_equality_independent: rule.

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

* canonical function_intro(level y): int tok rule.

function_equality_lambda(level z): int tok rule.

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

* noncanonical function_elim(hyp on y): int term tok rule.

function_elim_independent(hyp y): int tok rule.

function_equality_apply(using): term rule.

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

* equality extensionality(y): tok rule.

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

* computation function_computation(where): int rule.


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