Absolute value function

Uses Functions, Absolute value

It is often useful to have a function term (see Functions) for the absolute value:
 abs : (ℝ → ℝ.nn)

In rewriting, it is replaced by the equivalent operator:
 abs[x:ℝ] ⇒ abs(x)