diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-20 13:28:02 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-20 13:52:18 -0400 |
| commit | 6f7cb2dc6acc4e0aa00c80e550879ee36d35e6a4 (patch) | |
| tree | 17d0a2bc9c873c52573392b254669984e36b27c2 /src/Arithmetic/Saturated.v | |
| parent | 3807e854b302cfab34c68e41dd58fe3e284d1cbe (diff) | |
Remove duplicate [small p] hypothesis from small_conditional_sub
Diffstat (limited to 'src/Arithmetic/Saturated.v')
| -rw-r--r-- | src/Arithmetic/Saturated.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index 6d12bca0b..698b0d694 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -1052,7 +1052,7 @@ Section API. Lemma small_conditional_sub n mask (p:T (S n)) (q:T n) (psmall : small p) (qsmall : small q) (Hmask : Tuple.map (Z.land mask) q = q): - small p -> 0 <= eval p < eval q + (uweight bound n) -> + 0 <= eval p < eval q + (uweight bound n) -> small (conditional_sub mask p q). Admitted. |