next up previous contents
Next: Basic Semantics of Rule Up: The Tactic Language Previous: The Tactic Language

Predeclared Operators

The predeclared operators which implement the tactic language are the rule infixes =>, <=, =>> and <<=. There are additional related operators *>, <* and !! which will be explained below. The operators @ and , of function application and pairing have special roles in the tactic language as well. The predeclared operator = can be used as a theorem constructor. There are special unary ``delay'' operators # and ## explained below.

There are also predeclared mathematical operators +!, *!, -!, /!, %!, <!, and =! of unlimited precision unsigned integer arithmetic which are executed by the tactic interpreter.

A new predeclared operator : implements type labels as retractions onto ``strongly Cantorian sets''.

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997