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/Arithmetic/Partition.v | |
parent | ee30e8faf778ac9fd43f1d8d9d6d61cd4e9d8b3f (diff) |
partition -> Partition.partition to prevent confusion with List.partition
Diffstat (limited to 'src/Arithmetic/Partition.v')
-rw-r--r-- | src/Arithmetic/Partition.v | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/Arithmetic/Partition.v b/src/Arithmetic/Partition.v index 2d2fb87fa..ed2c45f9e 100644 --- a/src/Arithmetic/Partition.v +++ b/src/Arithmetic/Partition.v @@ -9,11 +9,15 @@ Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. Require Import Crypto.Util.Notations. Import ListNotations Weight. Local Open Scope Z_scope. -Section Partition. - Context weight {wprops : @weight_properties weight}. - - Definition partition n x := +(* extra name wrapper so partition won't be confused with List.partition *) +Module Partition. + Definition partition (weight : nat -> Z) n x := map (fun i => (x mod weight (S i)) / weight i) (seq 0 n). +End Partition. + +Section PartitionProofs. + Context weight {wprops : @weight_properties weight}. + Local Notation partition := (Partition.partition weight). Lemma partition_step n x : partition (S n) x = partition n x ++ [(x mod weight (S n)) / weight n]. @@ -124,6 +128,6 @@ Section Partition. autorewrite with zsimplify; reflexivity. Qed. -End Partition. +End PartitionProofs. Hint Rewrite length_partition length_recursive_partition : distr_length. -Hint Rewrite eval_partition using (solve [auto; distr_length]) : push_eval.
\ No newline at end of file +Hint Rewrite eval_partition using (solve [auto; distr_length]) : push_eval. |