1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
17 (* REDEX POINTER ************************************************************)
19 (* Policy: boolean metavariables: a, b
20 pointer metavariables: p, q
22 (* Note: this is a path in the tree representation of a term
23 in which abstraction nodes are omitted;
24 on application nodes, "false" means "proceed right"
25 and "true" means "proceed left"
27 definition rpointer: Type[0] ≝ list bool.
29 (* Note: precedence relation on redex pointers: p ≺ q
30 to serve as base for the order relations: p < q and p ≤ q *)
31 inductive rpprec: relation rpointer ≝
32 | rpprec_nil : ∀b,q. rpprec (◊) (b::q)
33 | rppprc_cons: ∀p,q. rpprec (false::p) (true::q)
34 | rpprec_comp: ∀b,p,q. rpprec p q → rpprec (b::p) (b::q)
35 | rpprec_skip: ∀p,q. rpprec (false::p) q → rpprec p q
38 interpretation "'precedes' on redex pointers"
39 'prec p q = (rpprec p q).
41 (* Note: this should go to core_notation *)
42 notation "hvbox(a break ≺ b)"
43 non associative with precedence 45
46 (* Note: this is p < q *)
47 interpretation "'less than' on redex pointers"
48 'lt p q = (TC rpointer rpprec p q).
50 (* Note: this is p ≤ q *)
51 interpretation "'less or equal to' on redex pointers"
52 'leq x y = (star rpointer x y).