diff options
Diffstat (limited to 'src/Util/ListUtil.v')
-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. |