From fe04d34c95b68bfa253631bfdfb61742e1bcf3b5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Dec 2018 16:13:43 -0500 Subject: Remove ListUtil.List.repeat We are no longer checking against Coq 8.5, and it's simpler to not have two versions of `List.repeat` floating around. --- src/Util/ListUtil.v | 23 ----------------------- 1 file changed, 23 deletions(-) (limited to 'src/Util') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index fb19ac1da..60899696d 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -178,29 +178,6 @@ Module Export List. Qed. End Facts. - Section Repeat. - - Variable A : Type. - Fixpoint repeat (x : A) (n: nat ) := - match n with - | O => [] - | S k => x::(repeat x k) - end. - - Theorem repeat_length x n: - length (repeat x n) = n. - Proof using Type. - induction n as [| k Hrec]; simpl; rewrite ?Hrec; reflexivity. - Qed. - - Theorem repeat_spec n x y: - In y (repeat x n) -> y=x. - Proof using Type. - induction n as [|k Hrec]; simpl; destruct 1; auto. - Qed. - - End Repeat. - Section Cutting. Variable A : Type. -- cgit v1.2.3