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 | |
parent | e11e69619a66ddbc908c393bb65a920b67b0d4a9 (diff) |
Add ZRange.opp
-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 ]. |