Term Destructors

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.