diff options
Diffstat (limited to 'src/Util/ZRange')
| -rw-r--r-- | src/Util/ZRange/Operations.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v index c73b991e8..71dc31e50 100644 --- a/src/Util/ZRange/Operations.v +++ b/src/Util/ZRange/Operations.v @@ -27,6 +27,10 @@ Module ZRange. := let (l, u) := eta v in r[ 0 ~> Z.max (Z.abs l) (Z.abs u) ]. + Definition opp (v : zrange) : zrange + := let (l, u) := eta v in + r[ -u ~> -l ]. + Definition map (f : Z -> Z) (v : zrange) : zrange := let (l, u) := eta v in r[ f l ~> f u ]. |