]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground_2/etc/lib/list.etc
ground_2 released and permanently renamed as ground
[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / etc / lib / list.etc
diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/list.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/list.etc
deleted file mode 100644 (file)
index 211238f..0000000
+++ /dev/null
@@ -1,7 +0,0 @@
-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).