]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap.etc
partial commit in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / etc / unwind2_rmap.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap.etc
new file mode 100644 (file)
index 0000000..7a18aa3
--- /dev/null
@@ -0,0 +1,5 @@
+include "delayed_updating/notation/functions/black_righttriangle_1.ma".
+
+interpretation
+  "unwind map (reversed path)"
+  'BlackRightTriangle p = (unwind2_rmap tr_id p).