EditorDoc Sections Nuprl Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
`absadj' kbd_absadjust

Search up for an instance of <ab lhs> == <ab rhs> then:
Adjust lhs to make it a reasonable left-hand-side of an operator definition with right-hand-side rhs.1. If the lhs is a var, its name will become the opid.2. If the lhs is blank, the (current_object ()) will become the opid.3. Edit slots will be eliminated from the lhs.4. Free vars and level expressions will be imported from the rhs if they aren't already in the lhs. New level exprs are added to the front, new parms and new term vars are added to the back.5. The arities of free vars from the rhs supercede the arities of free vars on the left with the same name.6. The bindings of the lhs are adjusted to match the arities of the var instances in their scope.The rhs will also be adjusted when it seems that a recursive definition is desired.7. If the lhs is blank, then blank terms on the rhs will be filled in with the new lhs.8. If the rhs contains instances of the lhs operator, they will be updated to instances of the new lhs.Move leading function arguments to the lhs, i.e. use applications on the lhs instead of lambdas on the rhs.

The main use is in building a definition, but note that this is a convenient way to build a new operator:
Just insert <ab lhs> == <ab rhs>, say with the `abs=' command, build the fake to contain the vars of the various arities and the op-parms and level-exprs you want in the operator, put the opid you want in the lhs, then use the adjuster.
Iterate until satisfied.

See `adj'.

About:
!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

EditorDoc Sections Nuprl Doc