diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-02-23 15:22:37 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-02-23 15:22:37 -0500 |
| commit | 9d1319323dfc8a788832aaa8e682eabc084bcafa (patch) | |
| tree | 9f241f3e3ddb2fba65c56d1702044031cde93653 /src/Util/ZRange | |
| parent | e11e69619a66ddbc908c393bb65a920b67b0d4a9 (diff) | |
Add ZRange.opp
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 ]. |