diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-26 09:57:52 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-06-26 10:02:10 -0400 |
| commit | 3794a3b93f8aee88f4daf75ba3dd09eabc25e857 (patch) | |
| tree | 7c68338c4427e55424b72641c6d8b74156ff6c57 /src/Arithmetic/Saturated.v | |
| parent | 96be40dde65c874e22581499d3a245edbabf3e41 (diff) | |
Add a comment for nonzero_cps
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 927369e5d..1591b37b8 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -681,6 +681,7 @@ Section API. Definition zero {n:nat} : T n := B.Positional.zeros n. + (** Returns 0 iff all limbs are 0 *) Definition nonzero_cps {n} (p : T n) {cpsT} (f : Z -> cpsT) : cpsT := CPSUtil.to_list_cps _ p (fun p => CPSUtil.fold_right_cps runtime_lor 0%Z p f). Definition nonzero {n} (p : T n) : Z @@ -748,7 +749,6 @@ Section API. Lemma nonzero_id n p {cpsT} f : @nonzero_cps n p cpsT f = f (@nonzero n p). Proof. cbv [nonzero nonzero_cps]. prove_id. Qed. - Lemma join0_id n p R f : @join0_cps n p R f = f (join0 p). Proof. cbv [join0_cps join0]. prove_id. Qed. |