Nuprl - doc for term sequences

EditorDoc Sections Nuprl Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
In the Nuprl system, for many purposes a term sequence will be represented by a term, using a binary operator as the catenator.

Let OP be an opid and a list of op-parameter values. Then we say a term T is an OP-representation of a certain term sequence as follows:

1. If T is an instance of an operator with OP as its opid and op-parm-values, and has no immediate subterms, then T represents the empty sequence.

2. If T is an instance of an operator with OP as its opid and op-parm-values, and has two-immediate subterms and no bindings, then T represents the catenation of the sequences represented by its subterms.

3. Otherwise, T represents the unit sequence with itself as the only member.

The system avoids ambiguity by expecting specific operator ids and op-parms to be used in specific places where term sequences are needed as data. The structure of the particular binary trees representing the sequences will be ignored for those purposes.

It often happens that a person wants to reorganize a term representing a sequence so that it represents the same sequence, but representing a certain segment with a single subterm.
To select a subsequence,

1. click `(m-(mousemiddle))' anywhere inside one term you want at the beginning or end, which will insert #MARK <term>,

2. then with this mark left highlighted, use the same command to click on the other endpoint; if you move the point off the #MARK <term> when you do the second `(m-(mousemiddle))', you'll just get another #MARK <term>.

2'. If you use `(c-a)(m-(mousemiddle))' instead, regrouping will work even through operators that merely have the same opid and sequence of parameter KINDS. This is useful when regrouping in WORDS contexts.

The smallest sequence representation containing these two subterms will be reorganized to get these elements into a single subterm presenting the segment with them as endpoints.

`norm'
You can also reorganize a sequence so that nesting is only through one place. The command `norm' will perform this nesting in the direction indicated by the left-/right-mode, toggled by `{(c-w)(m-w)(c-i)}'. But unlike most of edit commands, it uses the positioning according to the term structure rather than the display structure. IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

EditorDoc Sections Nuprl Doc

1.	If T is an instance of an operator with OP as its opid and op-parm-values, and has no immediate subterms, then T represents the empty sequence.
2.	If T is an instance of an operator with OP as its opid and op-parm-values, and has two-immediate subterms and no bindings, then T represents the catenation of the sequences represented by its subterms.
3.	Otherwise, T represents the unit sequence with itself as the only member.

1.	click `(m-(mousemiddle))' anywhere inside one term you want at the beginning or end, which will insert #MARK <term>,
2.	then with this mark left highlighted, use the same command to click on the other endpoint; if you move the point off the #MARK <term> when you do the second `(m-(mousemiddle))', you'll just get another #MARK <term>.
2'.	If you use `(c-a)(m-(mousemiddle))' instead, regrouping will work even through operators that merely have the same opid and sequence of parameter KINDS. This is useful when regrouping in WORDS contexts.