minor additions to standard library

[helm.git] / matita / matita / lib / lambda / etc / cons_r.etc

diff --git a/matita/matita/lib/lambda/etc/cons_r.etc b/matita/matita/lib/lambda/etc/cons_r.etc
new file mode 100644 (file)
index 0000000..46b2a08
--- /dev/null
+++ b/matita/matita/lib/lambda/etc/cons_r.etc
@@ -0,0 +1,7 @@
+notation "hvbox(l ⨭ break a)"
+  left associative with precedence 47
+  for @{'cons_r $l $a}.
+
+interpretation "" 'nil = (Atom).
+
+interpretation "" 'cons_r tl hd = (tl hd).