diff options
author | jadep <jade.philipoom@gmail.com> | 2019-04-03 14:45:32 -0400 |
---|---|---|
committer | jadephilipoom <jade.philipoom@gmail.com> | 2019-04-03 23:34:53 +0100 |
commit | bd34d676010ebf6dd4aa5076537f89572803dd3d (patch) | |
tree | bbc634fa51d071a4bd1e55019dc6853ecd936622 /src/PushButtonSynthesis/BarrettReduction.v | |
parent | ee30e8faf778ac9fd43f1d8d9d6d61cd4e9d8b3f (diff) |
partition -> Partition.partition to prevent confusion with List.partition
Diffstat (limited to 'src/PushButtonSynthesis/BarrettReduction.v')
-rw-r--r-- | src/PushButtonSynthesis/BarrettReduction.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/PushButtonSynthesis/BarrettReduction.v b/src/PushButtonSynthesis/BarrettReduction.v index 42be4b7d4..990a0de03 100644 --- a/src/PushButtonSynthesis/BarrettReduction.v +++ b/src/PushButtonSynthesis/BarrettReduction.v @@ -75,7 +75,7 @@ Section rbarrett_red. Lemma mut_correct : 0 < machine_wordsize -> - partition (uweight machine_wordsize) (1 + 1) (muLow + 2 ^ machine_wordsize) = [muLow; 1]. + Partition.partition (uweight machine_wordsize) (1 + 1) (muLow + 2 ^ machine_wordsize) = [muLow; 1]. Proof. intros; cbn. subst muLow. assert (0 < 2^machine_wordsize) by ZeroBounds.Z.zero_bounds. @@ -90,7 +90,7 @@ Section rbarrett_red. Lemma Mt_correct : 0 < machine_wordsize -> 2^(machine_wordsize - 1) < M < 2^machine_wordsize -> - partition (uweight machine_wordsize) 1 M = [M]. + Partition.partition (uweight machine_wordsize) 1 M = [M]. Proof. intros; cbn. assert (0 < 2^(machine_wordsize-1)) by ZeroBounds.Z.zero_bounds. rewrite !uweight_S, weight_0; auto using uwprops with lia. |