From d26dfb1ccdbb8448047d8932ae970daf1bc1d416 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 22 Feb 2016 14:50:48 +0100
Subject: [PATCH] add a notion of cons-ing a funcion, and notation for it

---
 prelude/functions.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/prelude/functions.v b/prelude/functions.v
index 2e4c93caa..bc12965f0 100644
--- a/prelude/functions.v
+++ b/prelude/functions.v
@@ -29,3 +29,26 @@ Section functions.
   Proof. unfold alter, fn_alter. by destruct (decide (a = b)). Qed.
 
 End functions.
+
+(** "Cons-ing" of functions from nat to T *)
+Section fcons.
+  Context {T : Type}.
+
+  Definition fn_cons (t : T) (f: nat → T) : nat → T :=
+    λ n, match n with
+         | O => t
+         | S n => f n
+         end.
+
+  Definition fn_mcons (ts : list T) (f : nat → T) : nat → T :=
+    fold_right fn_cons f ts.
+End fcons.
+
+Infix ".::" := fn_cons (at level 60, right associativity) : C_scope.
+Infix ".++" := fn_mcons (at level 60, right associativity) : C_scope.
+
+Lemma fn_mcons_app {T : Type} (ts1 ts2 : list T) f :
+  (ts1 ++ ts2) .++ f = ts1 .++ (ts2 .++ f).
+Proof.
+  unfold fn_mcons. rewrite fold_right_app. done.
+Qed.
-- 
GitLab