4.4 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 multiple 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 apply for all cases.

At the start of an operator body, options can declare precedence, associativity (in the case of an infix operator), and/or naming options. Each option keyword can appear at most once. The ~order option selects a operator order for the operator, which defines precedence relationships to other operator orders and a default associativity, but precedence and associativity options with operator override the ones defined with the operator order. In a precedence specification, a name refers to another operator binding or to a operator order, while ~other stands for any operator not otherwise mentioned. The ~name, ~who, and ~unsafe options are as in fun. When multiple cases are provided 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 options of a particular kind are in one or the other.