diff options
author | Jason Gross <jagro@google.com> | 2016-08-24 13:36:24 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-08-24 13:36:24 -0700 |
commit | 873d7be7f34814c5fee067a79a0ff0cdf739a54c (patch) | |
tree | ddd2fb85684ab45252a66bbf87e946d0c162d638 | |
parent | 25b95dd8547ec4cef48d55d84f39ee56230d5a1b (diff) |
Add map_cons from Coq 8.6
-rw-r--r-- | src/Util/ListUtil.v | 11 |
1 files changed, 11 insertions, 0 deletions
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. |