The built-in theorem `RAISE` implements the semantics of the `:`
unary operation on operators. In the case of ``flat'' operators
(left and right type 0), the effect is to implement all equations like

(?x@?z) + (?y@?z) = (?x :+ ?y) @ ?z;in other words, the effect of the colon operation is to produce a parallel operator on functions. The effect on operators with nontrivial relative type is the same in intent, but it is necessary to adjust types by appropriate introduction of constant function operators. The best way to find out how this works is by experiment. The

The built-in theorem `VALUE` takes a parameter, and is intended to
be applied to variable-binding contexts: the effect of applying `
VALUE @ [thm]` to `[term]` is the same as the effect of executing
`[thm => term]`. The reasons for the appearance of brackets around
the parameter are technical. Limitations of matching into variable
binding contexts originally forced this tactic to be provided as a
primitive. These limitations no longer obtain; an equivalent theorem
can be proved using limited higher-order matching.

Fri Sep 5 16:28:58 MDT 1997