-(*** Typing judgement ***)
-inductive JType : Env \to Term \to Typ \to Prop \def
- | T_Var : \forall G:Env.\forall x:nat.\forall T:Typ.
- (WFEnv G) \to (var_bind_in_env (mk_bound false x T) G) \to
- (JType G (Free x) T)
- | T_Abs : \forall G.\forall T1,T2:Typ.\forall t2:Term.
- \forall x:nat.
- (JType ((mk_bound false x T1)::G) (subst_term_O t2 (Free x)) T2) \to
- (JType G (Abs T1 t2) (Arrow T1 T2))
- | T_App : \forall G.\forall t1,t2:Term.\forall T2:Typ.
- \forall T1:Typ.(JType G t1 (Arrow T1 T2)) \to (JType G t2 T1) \to
- (JType G (App t1 t2) T2)
- | T_TAbs : \forall G:Env.\forall T1,T2:Typ.\forall t2:Term.
- \forall X:nat.
- (JType ((mk_bound true X T1)::G)
- (subst_term_tO t2 (TFree X)) (subst_type_O T2 (TFree X)))
- \to (JType G (TAbs T1 t2) (Forall T1 T2))
- | T_TApp : \forall G:Env.\forall t1:Term.\forall T2,T12:Typ.
- \forall X:nat.\forall T11:Typ.
- (JType G t1 (Forall T11 (subst_type_tfree_type T12 X (TVar O)))) \to
- (JSubtype G T2 T11)
- \to (JType G (TApp t1 T2) (subst_type_tfree_type T12 X T2))
- | T_Sub : \forall G:Env.\forall t:Term.\forall T:Typ.
- \forall S:Typ.(JType G t S) \to (JSubtype G S T) \to (JType G t T).
+notation "hvbox(e ⊢ break ta ⊴ break tb)"
+ non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.
+interpretation "Fsub subtype judgement" 'subjudg e ta tb =
+ (cic:/matita/Fsub/defn/JSubtype.ind#xpointer(1/1) e ta tb).
+
+notation > "hvbox(\Forall S.T)"
+ non associative with precedence 60 for @{ 'forall $S $T}.
+notation < "hvbox('All' \sub S. break T)"
+ non associative with precedence 60 for @{ 'forall $S $T}.
+interpretation "universal type" 'forall S T =
+ (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/5) S T).
+
+notation "#x" with precedence 79 for @{'tvar $x}.
+interpretation "bound tvar" 'tvar x =
+ (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/1) x).
+
+notation "!x" with precedence 79 for @{'tname $x}.
+interpretation "bound tname" 'tname x =
+ (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/2) x).
+
+notation "⊤" with precedence 90 for @{'toptype}.
+interpretation "toptype" 'toptype =
+ (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/3)).
+
+notation "hvbox(s break ⇛ t)"
+ right associative with precedence 55 for @{ 'arrow $s $t }.
+interpretation "arrow type" 'arrow S T =
+ (cic:/matita/Fsub/defn/Typ.ind#xpointer(1/1/4) S T).
+
+notation "hvbox(S [# n ↦ T])"
+ non associative with precedence 80 for @{ 'substvar $S $T $n }.
+interpretation "subst bound var" 'substvar S T n =
+ (cic:/matita/Fsub/defn/subst_type_nat.con S T n).
+
+notation "hvbox(|T|)"
+ non associative with precedence 30 for @{ 'tlen $T }.
+interpretation "type length" 'tlen T =
+ (cic:/matita/Fsub/defn/t_len.con T).
+
+notation > "hvbox(x ∈ l)"
+ non associative with precedence 30 for @{ 'inlist $x $l }.
+notation < "hvbox(x \nbsp ∈ \nbsp l)"
+ non associative with precedence 30 for @{ 'inlist $x $l }.
+interpretation "item in list" 'inlist x l =
+ (cic:/matita/Fsub/util/in_list.ind#xpointer(1/1) _ x l).
+
+notation "hvbox(!X ⊴ T)"
+ non associative with precedence 60 for @{ 'subtypebound $X $T }.
+interpretation "subtyping bound" 'subtypebound X T =
+ (cic:/matita/Fsub/defn/bound.ind#xpointer(1/1/1) true X T).
+
+(*notation < "hvbox(e break ⊢ ta \nbsp 'V' \nbsp tb (= \above \alpha))"
+ non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.
+notation > "hvbox(e break ⊢ ta 'Fall' break tb)"
+ non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.
+notation "hvbox(e break ⊢ ta \lessdot break tb)"
+ non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.*)