X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpointer.ma;h=30b4fdf6409b7690a05b7b7995e9592d92f90c20;hb=2e700622e2565c6695e8c1264dd4c1207896f28c;hp=8d7afa1aa877867ccdc567cb2d72a6b75d5f0d2b;hpb=178820be7648a60af17837727e51fd1f3f2791db;p=helm.git

diff --git a/matita/matita/contribs/lambda/pointer.ma b/matita/matita/contribs/lambda/pointer.ma
index 8d7afa1aa..30b4fdf64 100644
--- a/matita/matita/contribs/lambda/pointer.ma
+++ b/matita/matita/contribs/lambda/pointer.ma
@@ -12,18 +12,23 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "preamble.ma".
+include "term.ma".
 
 (* POINTER ******************************************************************)
 
 (* Policy: pointer step metavariables: c *)
 (* Note: this is a step of a path in the tree representation of a term:
-         rc (rectus)  : proceed on the argument of an abstraction
+         rc (rectus)  : not needed (we use sn instead)
          sn (sinister): proceed on the left argument of an application
+                        or on the argument of an abstraction (this would be rc)
          dx (dexter)  : proceed on the right argument of an application
 *)
+(* Remark: the following breaks destruct because of δ-expansions
+           definition ptr_step: Type[0] ≝ bool.
+           definition sn: bool ≝ true.
+           definition dx: bool ≝ false.
+*)
 inductive ptr_step: Type[0] ≝
-| rc: ptr_step
 | sn: ptr_step
 | dx: ptr_step
 .
@@ -43,3 +48,12 @@ lemma in_head_ind: ∀R:predicate ptr. R (◊) →
 #R #H #IH #p elim p -p // -H *
 #p #IHp * #H1 #H2 destruct /3 width=1/
 qed-.
+
+definition compatible_rc: predicate (ptr→relation term) ≝ λR.
+                          ∀p,A1,A2. R p A1 A2 → R (sn::p) (𝛌.A1) (𝛌.A2).
+
+definition compatible_sn: predicate (ptr→relation term) ≝ λR.
+                          ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A).
+
+definition compatible_dx: predicate (ptr→relation term) ≝ λR.
+                          ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2).