From 9d1319323dfc8a788832aaa8e682eabc084bcafa Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 23 Feb 2018 15:22:37 -0500 Subject: Add ZRange.opp --- src/Util/ZRange/Operations.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/Util/ZRange') 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 ]. -- cgit v1.2.3