diff options
Diffstat (limited to 'src/Util/ZRange/Operations.v')
| -rw-r--r-- | src/Util/ZRange/Operations.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v index c6f209e16..32924e6dc 100644 --- a/src/Util/ZRange/Operations.v +++ b/src/Util/ZRange/Operations.v @@ -31,6 +31,8 @@ Module ZRange. Lemma normalize'_eq : normalize = normalize'. Proof. reflexivity. Defined. + Definition size (v : zrange) : Z := upper (normalize v) - lower (normalize v). + Definition abs (v : zrange) : zrange := let (l, u) := eta v in r[ 0 ~> Z.max (Z.abs l) (Z.abs u) ]. |