From 3794a3b93f8aee88f4daf75ba3dd09eabc25e857 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 26 Jun 2017 09:57:52 -0400 Subject: Add a comment for nonzero_cps --- src/Arithmetic/Saturated.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Arithmetic/Saturated.v') 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. -- cgit v1.2.3