Monus Operator

[smithnormform]

It could be nice to have a monus operator in Cryptol. Monus is defined by a monus b = if a > b then a - b else 0. According to this Wikipedia article, monus is usually denoted by ∸. You can already implement a monus b in Cryptol with max a b - b, so this would just be syntactic sugar (maybe denoted by *-).

This handy trick can come up when writing recursive functions or really any functions involving degenerate cases.

However, perhaps most of the monus use cases that come to mind could be resolved with some kind of GADT-style pattern matching.

[brianhuffman]

No language extensions are necessary for this; you can just define it, either on the value level, the type level, or both.

infixl 80 *-

type a *- b = max a b - b

(*-) : {a} (Cmp a, Ring a) =>
a *- b = if a > b then a - b else zero

You could also use the Unicode symbol for it if you like.