abs -package:Agda

Absolute value.
Compute the absolute value.
The absolute value of a number.
\a -> abs a * signum a ~= a
>>> abs (-1)
1
abs x1 returns the absolute value of x1. The term is expected to have type Int.
Construct an 'Abs fd' from a String.
Takes the absolute value of a Quantity.
Takes the absolute value of a possibly scaled SQuantity, preserving any scale factor.
The absolute tolerance. Defaults to 1e-12.
An absolute path.
Hack so that norms have a sensible type.