Absolute value

Uses Real numbers

The absolute value of any real number is a non-negative real number:
 abs(ℝ) : ℝ.nn

Special cases for the rational numbers and the integers:
 abs(ℚ) : ℚ.nn
 abs(ℤ) : ℕ

Special cases for the non-zero numbers are also useful:
 abs(ℝ.nz) : ℝ.p
 abs(ℚ.nz) : ℚ.p
 abs(ℤ.nz) : ℕ.nz

Simplification rules

The absolute value of a non-negative number is the number itself:
 abs(x:ℝ.nn) ⇒ x
 abs(x:ℝ) ⇒ x | x ≥ 0

For a negative number, it is the negative:
 abs(x:ℝ) ⇒ -(x) | x < 0

Examples

Given:
 _example aPositiveNumber : ℝ.p
 _example aNegativeNumber : ℝ with _example aNegativeNumber < 0 ⇒ ⊤
 _example anUnknownNumber : ℝ

We find:
 _example abs(aPositiveNumber) ⇒ aPositiveNumber
 _example abs(aNegativeNumber) ⇒ -(aNegativeNumber)
 _example abs(anUnknownNumber) ⇒ abs(anUnknownNumber)

For literals:
 _example abs(2) ⇒ 2
 _example abs(-2/3) ⇒ 2/3