diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-12-04 16:36:18 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-12-04 16:36:18 -0500 |
| commit | 8742bd10f88593091dd45f99dd1b2358b8ac4000 (patch) | |
| tree | fa0514484a2d26f4f6abca182f931b80698fa7d5 /src | |
| parent | 066702a2eeba8ab6a662461f2e9c7343927919e1 (diff) | |
More repeat fixing
Diffstat (limited to 'src')
| -rw-r--r-- | src/LegacyArithmetic/Double/Proofs/Decode.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/LegacyArithmetic/Double/Proofs/Decode.v b/src/LegacyArithmetic/Double/Proofs/Decode.v index c0748cf8e..5b3445208 100644 --- a/src/LegacyArithmetic/Double/Proofs/Decode.v +++ b/src/LegacyArithmetic/Double/Proofs/Decode.v @@ -22,7 +22,7 @@ Section decode. Context {n W} {decode : decoder n W}. Section with_k. Context {k : nat}. - Local Notation limb_widths := (repeat n k). + Local Notation limb_widths := (List.repeat n k). Lemma decode_bounded {isdecode : is_decode decode} w : 0 <= n -> Pow2Base.bounded limb_widths (List.map decode (rev (to_list k w))). @@ -56,7 +56,7 @@ Section decode. End with_k. Local Arguments Pow2Base.base_from_limb_widths : simpl never. - Local Arguments repeat : simpl never. + Local Arguments List.repeat : simpl never. Local Arguments Z.mul !_ !_. Lemma tuple_decoder_S {k} w : 0 <= n -> (tuple_decoder (k := S (S k)) w = tuple_decoder (k := S k) (fst w) + (decode (snd w) << (S k * n)))%Z. Proof using Type. |