ground_2 released and permanently renamed as ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / etc / lib / list.etc

diff --git a/matita/matita/contribs/lambdadelta/ground/etc/lib/list.etc b/matita/matita/contribs/lambdadelta/ground/etc/lib/list.etc
new file mode 100644 (file)
index 0000000..211238f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/etc/lib/list.etc
@@ -0,0 +1,7 @@
+let rec append A (l1: list A) l2 on l1 ≝
+  match l1 with
+  [ nil        ⇒ l2
+  | cons hd tl ⇒ hd :: append A tl l2
+  ].
+
+interpretation "append (list)" 'Append l1 l2 = (append ? l1 l2).