From 873d7be7f34814c5fee067a79a0ff0cdf739a54c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 Aug 2016 13:36:24 -0700 Subject: Add map_cons from Coq 8.6 --- src/Util/ListUtil.v | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 06e7206cd..9c263eed9 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -49,6 +49,17 @@ Module Export List. Local Set Implicit Arguments. Import ListNotations. (** From the 8.6 Standard Library *) + + Section Map. + Variables (A : Type) (B : Type). + Variable f : A -> B. + + Lemma map_cons (x:A)(l:list A) : map f (x::l) = (f x) :: (map l). + Proof. + reflexivity. + Qed. + End Map. + Lemma in_seq len start n : In n (seq start len) <-> start <= n < start+len. Proof. -- cgit v1.2.3