<conditions>
<ab lhs> == <ab rhs>

or like this, when there are no conditions:

<ab lhs> == <ab rhs>

Recursive definitions are permitted (they are automatically translated to non-recursive form using the Y-combinator).

The operator definition does not take effect until a successful "verification" has been performed, typically with the `(c-v)' command which will also checks for coherency and raises a utility for developing auxilliary objects such as display forms and typing-theorems. doc for abs verify

The "conditions" are used by the system and the editor for various purposes, but for normal mathematical operators, there will usually be no conditions attached to the definition. doc for term sequences

If you need to reveal the hidden conditions slot in order to add some conditions, just use `(c-s)' on the defintion form. `(c-t)' and identifers will insert a condition in a condition slot; `(c-(space))' will insert <conds>, <conds>

If the right-hand-side of the definition is PRIMITIVE, then the ABS object merely declares the operator without defining it to expand to anything.

There is a small utility menu for editing ABS objects, which you can raise with the `absedit' command or, if you are focussed on an ABS window, with the `{ededit}' command.

The easiest way to create an operator definition is to fill in the right-hand-side with the definiens, then use the `adj' command, which will adjust the left-hand-side so that it makes sense with respect to the right hand side; and when the definition is recursive, the rhs may be adjusted as well. HERE for detail on adjusting.
Even if you just want to declare a primitive operator, it is usually easiest to make up a bogus rhs to force the lhs, and then replace the right-hand-side by PRIMITIVE.

Inserting new operators without defining or declaring them: It is also possible to insert <ab lhs> == <ab rhs> directly anywhere with the `abs=' command. This is the recommended procedure for inserting an operator which has no definition and no available examples. You create the term indirectly using `adj' on the "definition" until the left-side is the term you want, then replace the abs-equality by the left-hand-side, say with the `(c-u)(c-(space))' command applied to the left-hand-side.

DO Review cmds for group: "Abs"

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