diff options
| author | Brian Campbell | 2018-07-07 15:17:20 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-07 15:17:20 +0100 |
| commit | 2a2f38f46735a81a921891bf0bf9e35a7cc4a347 (patch) | |
| tree | 0d7a403c0e40efa40ad49eb0906fe06c3e33d0c0 /lib/coq | |
| parent | 7c36a2c621ce64e3a181bf72f7b0434f42450092 (diff) | |
Coq: eq_range should take proofs
Diffstat (limited to 'lib/coq')
| -rw-r--r-- | lib/coq/Sail2_values.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 990817e6..db0339d8 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1368,6 +1368,8 @@ Definition abs_with_eq n : {o : Z & ArithFact (o = Z.abs n)} := build_ex (Z.ab (* Similarly, for ranges (currently in MIPS) *) +Definition eq_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)}) : bool := + (projT1 l) =? (projT1 r). Definition add_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)}) : {x & ArithFact (n+o <= x <= m+p)} := build_ex ((projT1 l) + (projT1 r)). |