6.7 Operators🔗ℹ

The operator is function-like in the sense that it receives argument values. (To bind an operator that is not function-like, see macro or expr.macro.) Each argument is specified by a binding that must be written as a single shrubbery term that is not an operator in the shrubbery sense; parentheses can be used around other binding forms for arguments. If two identifier terms appear within the parentheses that follow operator, a prefix operator is defined using the first identifier as its name. When a parenthesized sequence is followed by :: or :~, it is treated as starting a maybe_res_annot, which is the same as in fun definitions.

The new operator is also bound a repetition operator, in which case its arguments must be repetitions. The depth of the resulting repetition is the maximum of the argument repetition depths.

When multple cases are provided via |, an operator can be defined as both prefix and infix or prefix and postfix (but not infix and postfix). The prefix cases and infix/postfix cases can be mixed in any order, but when the operator is used as a prefix or infix/postfix operator, cases are tried in the relative order that they are written. Similar to the fun form the operator name and a result annotation can be written before the | cases to appply for all cases.

At the start of an operator body, options can declare precedence and, in the case of an infix operator, an associativity for the operator. Each option keyword can appear at most once. In a precedence specification, ~other stands for any operator not otherwise mentioned. When multiple cases are povided using an immediate |, then only the first prefix case and the first infix/postfix case can supply options; alternatively, when the operator name (maybe with a result annotation) is written before |, options that apply to all cases can be supplied in a block before the cases. Options can appear both before the cases and in individual clauses, as long as all precedence and all associatvity options are in one or the other.