- we introduced the pointer_step rc in the perspective of proving

[helm.git] / matita / matita / contribs / lambda / pointer.ma

diff --git a/matita/matita/contribs/lambda/pointer.ma b/matita/matita/contribs/lambda/pointer.ma
index 27f30b22c199a2d47544019c18b6e482174e09e0..d71574e744123ba51a836db8443f36dbf7e09627 100644 (file)
--- a/matita/matita/contribs/lambda/pointer.ma
+++ b/matita/matita/contribs/lambda/pointer.ma
@@ -18,17 +18,12 @@ include "term.ma".
 
 (* Policy: pointer step metavariables: c *)
 (* Note: this is a step of a path in the tree representation of a term:
-         rc (rectus)  : not needed (we use sn instead)
+         rc (rectus)  : proceed on the argument of an abstraction
          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
 .
@@ -50,7 +45,7 @@ lemma in_whd_ind: ∀R:predicate ptr. R (◊) →
 qed-.
 
 definition compatible_rc: predicate (ptr→relation term) ≝ λR.
-                          ∀p,A1,A2. R p A1 A2 → R (sn::p) (𝛌.A1) (𝛌.A2).
+                          ∀p,A1,A2. R p A1 A2 → R (rc::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).