]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/LOGIC/CLE/defs.ma
7a2c7606caf79d7b86c82b110d4e30159cf05755
[helm.git] / 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).