IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Exploding a term generates another term that represents the main operator in a way that makes the operator structure explicitly viewable and editable.
Use `(c-a)(c-s)' to explode or implode the point.
For example, exploding the term x:A. B(x) gives
IMPLODE all(A; x.B(x))
which shows the opid, and the subterms with bindings.
Exploding the term 12 gives IMPLODE natural_number{12:n}, showing its opid, and revealing that it has no subterms, and that it has a single n-type text slot.
The display forms for the exploded term representation elide empty sequences of components, such as empty parameter sequences, term sequences, and binding var sequences.
Use `(c-s)' to reveal such elisions.
The main uses of explode forms are:
1.
temporarily revealing the operator structure of a term whose display form is unfamiliar
2.
getting access to the opid as text for use in editing
3.
making a term-matching pattern to be used with an ML utility described in docforeditmatch
4.
modifying the operator in simple ways such as changing the opid, and permuting or deleting components; for other operator structure modification, as well as for creation of an operator for which you have no sample, the commands for "adjusting" operators are handier. See `absadj', `adj', and `newop'.
Usually `(mouseleft)' will implode it as well, which is why the mnemonic "IMPLODE" is used in the display. ML contexts are an exception since the explode form is often used in ML code in term-matching patterns, or as part of a crude quotation device; and since explode forms may be nested to form a term-matching pattern, being inside an explode form is also an exception. docforeditmatch
You can get a palette of editing buttons appropriate to the explode form with the command `expledit', or `{ededit}' if you are already pointing to an explode form. The palette will be inserted as a cover.
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
x:A. B(x)all(A; x.B(x))
edit}'
