From bd34d676010ebf6dd4aa5076537f89572803dd3d Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 3 Apr 2019 14:45:32 -0400 Subject: partition -> Partition.partition to prevent confusion with List.partition --- src/Arithmetic/Partition.v | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) (limited to 'src/Arithmetic/Partition.v') 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. -- cgit v1.2.3