`term_kind: term -> tok`.-
Returns the kind of the term. Possible results are:
`UNIVERSE`,`VOID`,`ANY`,`ATOM`,`TOKEN`,`INT`,`NATURAL-NUMBER`,`MINUS`,`ADDITION`,`SUBTRACTION`,`MULTIPLICATION`,`DIVISION`,`MODULO`,`INTEGER-INDUCTION`,`LIST`,`NIL`,`CONS`,`LIST-INDUCTION`,`UNION`,`INL`,`INR`,`DECIDE`,`PRODUCT`,`PAIR`,`SPREAD`,`FUNCTION`,`LAMBDA`,`APPLY`,`QUOTIENT`,`SET`,`EQUAL`,`AXIOM`,`VAR`,`BOUND-ID`,`TERM-OF-THEOREM`,`ATOMEQ`,`INTEQ`,`INTLESS`.There are corresponding predicates such as

`is_universe_term`and corresponding constructors such as`make_function_term`(which has type`tok term term term`). `destruct_universe: term int`.-
The integer is the universe
level.
`destruct_any: term term`.-
`destruct_token: term tok`.-
`destruct_natural_number: term int`.-
`destruct_minus: term term`.-
`destruct_addition: term (term # term)`.-

The results are the left and right terms. `destruct_subtraction: term (term # term)`.-
`destruct_multiplication: term (term # term)`.-
`destruct_division: term (term # term)`.-
`destruct_modulo: term (term # term)`.-
`destruct_integer_induction: term (term # term # term #\ term)`.-

The results are the value, down term, base term and up term. `destruct_list: term term`.-
Returns the type of the list.
`destruct_cons: term (term # term)`.-
Returns the head and
tail.
`destruct_list_induction: term (term # term # term)`.-

Returns the value, base term and up term. `destruct_union: term (term # term)`.-

Results in the left and right types. `destruct_inl: term term`.-
`destruct_inr: term term`.-
`destruct_decide: term (term # term # term)`.-

The result is the value, the left term and the right term. `destruct_product: term (tok # term # term)`.-

The result is the bound identifier, the left term and the right term. `destruct_pair: term (term # term)`.-

Returns the left term and the right term. `destruct_spread: term (term # term)`.-

Returns the value and the term. `destruct_function: term (tok # (term # term))`.-

The result is the bound identifier, the left term and the right term. `destruct_lambda: term (tok # term)`.-

Returns the bound identifier and the term. `destruct_apply: term (term # term)`.-

Returns the function and the argument. `destruct_quotient: term (tok # (tok # (term # term)))`.-

Returns the two bound identifiers, the left type and the right type. `destruct_set: term (tok # (term # term))`.-

Returns the bound identifier, the left type and the right type. `destruct_var: term tok`.-
`destruct_equal: term ((term list) # term)`.-

Returns a list of the equal terms and the type of the equality. `destruct_less: term (term # term))`.-

Returns the left term and the right term. `destruct_bound_id: term ((tok list) # term)`.-

Returns a list of the bound identifiers and the type. `destruct_term_of_theorem: term tok`.-

Returns the name of the theorem. `destruct_atomeq: term (term # (term # (term # term)))`.-

Returns the left term, right term, if term and else term. `destruct_inteq: term (term # (term # (term # term)))`.-

Returns the left term, right term, if term and else term. `destruct_intless: term (term # (term # (term # term)))`.-

Returns the left term, right term, if term and else term. `destruct_tagged: term (int # term)`.-

The integer returned is zero if the tag is`*`.

For each term type there is a corresponding constructor that is the curried inverse to the destructor given above. For example,

make_inteq_term: term term term term term.

Thu Sep 14 08:45:18 EDT 1995