matita/contribs/LOGIC/CLE/defs.ma

   1 set "baseuri" "cic:/matita/LOGIC/CLE/defs".
   2
   3 (* ORDER RELATION BETWEEN POSITIONS AND CONTEXTS
   4 *)
   5
   6 include "datatypes/Context.ma".
   7
   8 inductive CLE: Nat \to Context \to Prop \def
   9    | cle_zero: \forall Q. CLE zero Q
  10    | cle_succ: \forall Q,R,i. CLE i Q \to CLE (succ i) (abst Q R)
  11 .
  12
  13 interpretation "order relation between positions and contexts"
  14    'leq x y = (cic:/matita/LOGIC/CLE/defs/CLE.ind#xpointer(1/1) x y).