interpretation "three" 'three = (Var (S (S (S O)))).
notation "π" non associative with precedence 90 for @{ 'four }.
interpretation "four" 'four = (Var (S (S (S (S O))))).
-notation < "a Βb" left associative with precedence 60 for @{ 'appl $a $b }.
+notation < "a Βb" left associative with precedence 65 for @{ 'appl $a $b }.
interpretation "appl" 'appl a b = (Appl a b).
let rec lift (from:nat) (amount:nat) (what:PT) on what : PT β
notation < "| T |" with precedence 25 for @{'abs $T}.
interpretation "Fsub named type length" 'abs T = (nt_len T).
interpretation "list length" 'abs l = (length ? l).
-notation < "β©a,bβͺ Β· T" with precedence 60 for @{'swap $a $b $T}.
+notation < "β©a,bβͺ Β· T" with precedence 65 for @{'swap $a $b $T}.
interpretation "natural swap" 'swap a b n = (swap a b n).
interpretation "Fsub name swap in a named type" 'swap a b T = (swap_NTyp a b T).
interpretation "Fsub name swap in a LN type" 'swap a b T = (swap_Typ a b T).
interpretation "Fsub WF type judgement" 'wftjudg e t = (WFType e t).
notation > "\Forall S.T"
- non associative with precedence 60 for @{ 'forall $S $T}.
+ non associative with precedence 65 for @{ 'forall $S $T}.
notation < "hvbox(β \sub S. break T)"
- non associative with precedence 60 for @{ 'forall $S $T}.
+ non associative with precedence 65 for @{ 'forall $S $T}.
interpretation "universal type" 'forall S T = (Forall S T).
notation "#x" with precedence 79 for @{'tvar $x}.
interpretation "toptype" 'toptype = Top.
notation "hvbox(s break β t)"
- right associative with precedence 55 for @{ 'arrow $s $t }.
+ right associative with precedence 60 for @{ 'arrow $s $t }.
interpretation "arrow type" 'arrow S T = (Arrow S T).
notation "hvbox(S [#n β¦ T])"
interpretation "subst bound var" 'substvar S T n = (subst_type_nat S T n).
notation "hvbox(!X β΄ T)"
- non associative with precedence 60 for @{ 'subtypebound $X $T }.
+ non associative with precedence 65 for @{ 'subtypebound $X $T }.
interpretation "subtyping bound" 'subtypebound X T = (mk_bound true X T).
(****** PROOFS ********)
interpretation "Fsub subtype judgement" 'subjudg e ta tb = (JSubtype e ta tb).
notation > "hvbox(\Forall S.T)"
- non associative with precedence 60 for @{ 'forall $S $T}.
+ non associative with precedence 65 for @{ 'forall $S $T}.
notation < "hvbox('All' \sub S. break T)"
- non associative with precedence 60 for @{ 'forall $S $T}.
+ non associative with precedence 65 for @{ 'forall $S $T}.
interpretation "universal type" 'forall S T = (Forall S T).
notation "#x" with precedence 79 for @{'tvar $x}.
interpretation "toptype" 'toptype = Top.
notation "hvbox(s break β t)"
- right associative with precedence 55 for @{ 'arrow $s $t }.
+ right associative with precedence 60 for @{ 'arrow $s $t }.
interpretation "arrow type" 'arrow S T = (Arrow S T).
notation "hvbox(β΄ T)"
- non associative with precedence 60 for @{ 'subtypebound $T }.
+ non associative with precedence 65 for @{ 'subtypebound $T }.
interpretation "subtyping bound" 'subtypebound T = (mk_bound true T).
(****** PROOFS ********)
[ apply (q_lt_corefl ? H)| cases (q_lt_le_incompat ?? (q_neg_gt ?) (q_lt_to_le ?? H))]
qed.
-notation < "x \blacksquare" non associative with precedence 50 for @{'unpos $x}.
+notation < "x \blacksquare" non associative with precedence 55 for @{'unpos $x}.
interpretation "hide unpos proof" 'unpos x = (unpos x ?).
interpretation "real opp" 'uminus x = (Ropp x).
notation "hvbox(a break Β· b)"
- right associative with precedence 55
+ right associative with precedence 60
for @{ 'mult $a $b }.
interpretation "real mult" 'mult x y = (Rmult x y).
definition member_of : βX.set X β X β Propβ Ξ»X.Ξ»A:set X.Ξ»x.A x.
-notation "hvbox(x break β A)" with precedence 60
+notation "hvbox(x break β A)" with precedence 65
for @{ 'member_of $x $A }.
interpretation "Member of" 'member_of x A = (mk_member_of ? A x).
-notation "hvbox(x break β A)" with precedence 60
+notation "hvbox(x break β A)" with precedence 65
for @{ 'not_member_of $x $A }.
interpretation "Not member of" 'not_member_of x A = (Not (member_of ? A x)).
definition subset: βX. set X β set X β Propβ Ξ»X.Ξ»A,B:set X.βx. x β A β x β B.
-notation "hvbox(A break β B)" with precedence 60
+notation "hvbox(A break β B)" with precedence 65
for @{ 'subset $A $B }.
interpretation "Subset" 'subset A B = (subset ? A B).
definition union: βX. set X β set X β set X β Ξ»X.Ξ»A,B:set X.Ξ»x. x β A β¨ x β B.
-notation "hvbox(A break βͺ B)" with precedence 65
+notation "hvbox(A break βͺ B)" with precedence 66
for @{ 'union $A $B }.
interpretation "Union" 'union A B = (union ? A B).
definition countable_union: βX. seq (set X) β set X β
Ξ»X.Ξ»A:seq (set X).Ξ»x.βj.x β A \sub j.
-notation "βͺ \sub (ident i opt (: ty)) B" with precedence 65
+notation "βͺ \sub (ident i opt (: ty)) B" with precedence 66
for @{ 'big_union ${default @{(Ξ»${ident i}:$ty.$B)} @{(Ξ»${ident i}.$B)}}}.
interpretation "countable_union" 'big_union Ξ·.t = (countable_union ? t).
ap_cotransitive: cotransitive ? ap_apart
}.
-notation "hvbox(a break # b)" non associative with precedence 50 for @{ 'apart $a $b}.
+notation "hvbox(a break # b)" non associative with precedence 55 for @{ 'apart $a $b}.
interpretation "apartness" 'apart x y = (ap_apart ? x y).
definition apartness_of_excess_base: excess_base β apartness.
definition eq β Ξ»A:apartness.Ξ»a,b:A. Β¬ (a # b).
-notation "hvbox(a break β b)" non associative with precedence 50 for @{ 'napart $a $b}.
+notation "hvbox(a break β b)" non associative with precedence 55 for @{ 'napart $a $b}.
interpretation "Apartness alikeness" 'napart a b = (eq ? a b).
interpretation "Excess alikeness" 'napart a b = (eq (excess_base_OF_excess1 ?) a b).
interpretation "Excess (dual) alikeness" 'napart a b = (eq (excess_base_OF_excess ?) a b).
lemma eq_trans:βE:apartness.βx,z,y:E.x β y β y β z β x β z β
Ξ»E,x,y,z.eq_trans_ E x z y.
-notation > "'Eq'β" non associative with precedence 50 for @{'eqrewrite}.
+notation > "'Eq'β" non associative with precedence 55 for @{'eqrewrite}.
interpretation "eq_rew" 'eqrewrite = (eq_trans ? ? ?).
alias id "antisymmetric" = "cic:/matita/constructive_higher_order_relations/antisymmetric.con".
intro Xyz; apply Exy; apply exc2ap; left; assumption;
qed.
-notation > "'Le'βͺ" non associative with precedence 50 for @{'lerewritel}.
+notation > "'Le'βͺ" non associative with precedence 55 for @{'lerewritel}.
interpretation "le_rewl" 'lerewritel = (le_rewl ? ? ?).
-notation > "'Le'β«" non associative with precedence 50 for @{'lerewriter}.
+notation > "'Le'β«" non associative with precedence 55 for @{'lerewriter}.
interpretation "le_rewr" 'lerewriter = (le_rewr ? ? ?).
lemma ap_rewl: βA:apartness.βx,z,y:A. x β y β y # z β x # z.
apply ap_symmetric; assumption;
qed.
-notation > "'Ap'βͺ" non associative with precedence 50 for @{'aprewritel}.
+notation > "'Ap'βͺ" non associative with precedence 55 for @{'aprewritel}.
interpretation "ap_rewl" 'aprewritel = (ap_rewl ? ? ?).
-notation > "'Ap'β«" non associative with precedence 50 for @{'aprewriter}.
+notation > "'Ap'β«" non associative with precedence 55 for @{'aprewriter}.
interpretation "ap_rewr" 'aprewriter = (ap_rewr ? ? ?).
alias symbol "napart" = "Apartness alikeness".
elim (Exy); apply exc2ap; left; assumption;
qed.
-notation > "'Ex'βͺ" non associative with precedence 50 for @{'excessrewritel}.
+notation > "'Ex'βͺ" non associative with precedence 55 for @{'excessrewritel}.
interpretation "exc_rewl" 'excessrewritel = (exc_rewl ? ? ?).
-notation > "'Ex'β«" non associative with precedence 50 for @{'excessrewriter}.
+notation > "'Ex'β«" non associative with precedence 55 for @{'excessrewriter}.
interpretation "exc_rewr" 'excessrewriter = (exc_rewr ? ? ?).
lemma lt_rewr: βA:excess.βx,z,y:A. x β y β z < y β z < x.
[apply (Leβͺ ? (eq_sym ??? E));| apply (Apβͺ ? E);] assumption;
qed.
-notation > "'Lt'βͺ" non associative with precedence 50 for @{'ltrewritel}.
+notation > "'Lt'βͺ" non associative with precedence 55 for @{'ltrewritel}.
interpretation "lt_rewl" 'ltrewritel = (lt_rewl ? ? ?).
-notation > "'Lt'β«" non associative with precedence 50 for @{'ltrewriter}.
+notation > "'Lt'β«" non associative with precedence 55 for @{'ltrewriter}.
interpretation "lt_rewr" 'ltrewriter = (lt_rewr ? ? ?).
lemma lt_le_transitive: βA:excess.βx,y,z:A.x < y β y β€ z β x < z.
definition increasing β Ξ»O:excess.Ξ»a:sequence O.βn:nat.a n β€ a (S n).
-notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 for @{'upper_bound $_ $s $x}.
-notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 for @{'lower_bound $_ $s $x}.
-notation < "s \nbsp 'is_increasing'" non associative with precedence 50 for @{'increasing $_ $s}.
-notation < "s \nbsp 'is_decreasing'" non associative with precedence 50 for @{'decreasing $_ $s}.
-notation < "x \nbsp 'is_strong_sup' \nbsp s" non associative with precedence 50 for @{'strong_sup $_ $s $x}.
-notation < "x \nbsp 'is_strong_inf' \nbsp s" non associative with precedence 50 for @{'strong_inf $_ $s $x}.
-
-notation > "x 'is_upper_bound' s 'in' e" non associative with precedence 50 for @{'upper_bound $e $s $x}.
-notation > "x 'is_lower_bound' s 'in' e" non associative with precedence 50 for @{'lower_bound $e $s $x}.
-notation > "s 'is_increasing' 'in' e" non associative with precedence 50 for @{'increasing $e $s}.
-notation > "s 'is_decreasing' 'in' e" non associative with precedence 50 for @{'decreasing $e $s}.
-notation > "x 'is_strong_sup' s 'in' e" non associative with precedence 50 for @{'strong_sup $e $s $x}.
-notation > "x 'is_strong_inf' s 'in' e" non associative with precedence 50 for @{'strong_inf $e $s $x}.
+notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 55 for @{'upper_bound $_ $s $x}.
+notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 55 for @{'lower_bound $_ $s $x}.
+notation < "s \nbsp 'is_increasing'" non associative with precedence 55 for @{'increasing $_ $s}.
+notation < "s \nbsp 'is_decreasing'" non associative with precedence 55 for @{'decreasing $_ $s}.
+notation < "x \nbsp 'is_strong_sup' \nbsp s" non associative with precedence 55 for @{'strong_sup $_ $s $x}.
+notation < "x \nbsp 'is_strong_inf' \nbsp s" non associative with precedence 55 for @{'strong_inf $_ $s $x}.
+
+notation > "x 'is_upper_bound' s 'in' e" non associative with precedence 55 for @{'upper_bound $e $s $x}.
+notation > "x 'is_lower_bound' s 'in' e" non associative with precedence 55 for @{'lower_bound $e $s $x}.
+notation > "s 'is_increasing' 'in' e" non associative with precedence 55 for @{'increasing $e $s}.
+notation > "s 'is_decreasing' 'in' e" non associative with precedence 55 for @{'decreasing $e $s}.
+notation > "x 'is_strong_sup' s 'in' e" non associative with precedence 55 for @{'strong_sup $e $s $x}.
+notation > "x 'is_strong_inf' s 'in' e" non associative with precedence 55 for @{'strong_inf $e $s $x}.
interpretation "Excess upper bound" 'upper_bound e s x = (upper_bound e s x).
interpretation "Excess lower bound" 'lower_bound e s x = (upper_bound (dual_exc e) s x).
sl_strong_extop: βx.strong_ext ? (sl_op x)
}.
-notation "a \cross b" left associative with precedence 50 for @{ 'op $a $b }.
+notation "a \cross b" left associative with precedence 55 for @{ 'op $a $b }.
interpretation "semi lattice base operation" 'op a b = (sl_op ? a b).
lemma excess_of_semi_lattice_base: semi_lattice_base β excess.
definition hole β Ξ»T:Type.Ξ»x:T.x.
-notation < "\ldots" non associative with precedence 50 for @{'hole}.
+notation < "\ldots" non associative with precedence 55 for @{'hole}.
interpretation "hole" 'hole = (hole ? ?).
(* SL(E,M,H2-5(#),H67(β°)) β E' β c E = c E' β H67'(β°') β SL(E,M,p2-5,H67') *)
absorbmj: βf,g:latt_carr. (f β§ (f β¨ g)) β f
}.
-notation "'meet'" non associative with precedence 50 for @{'meet}.
-notation "'meet_refl'" non associative with precedence 50 for @{'meet_refl}.
-notation "'meet_comm'" non associative with precedence 50 for @{'meet_comm}.
-notation "'meet_assoc'" non associative with precedence 50 for @{'meet_assoc}.
-notation "'strong_extm'" non associative with precedence 50 for @{'strong_extm}.
-notation "'le_to_eqm'" non associative with precedence 50 for @{'le_to_eqm}.
-notation "'lem'" non associative with precedence 50 for @{'lem}.
-notation "'join'" non associative with precedence 50 for @{'join}.
-notation "'join_refl'" non associative with precedence 50 for @{'join_refl}.
-notation "'join_comm'" non associative with precedence 50 for @{'join_comm}.
-notation "'join_assoc'" non associative with precedence 50 for @{'join_assoc}.
-notation "'strong_extj'" non associative with precedence 50 for @{'strong_extj}.
-notation "'le_to_eqj'" non associative with precedence 50 for @{'le_to_eqj}.
-notation "'lej'" non associative with precedence 50 for @{'lej}.
+notation "'meet'" non associative with precedence 55 for @{'meet}.
+notation "'meet_refl'" non associative with precedence 55 for @{'meet_refl}.
+notation "'meet_comm'" non associative with precedence 55 for @{'meet_comm}.
+notation "'meet_assoc'" non associative with precedence 55 for @{'meet_assoc}.
+notation "'strong_extm'" non associative with precedence 55 for @{'strong_extm}.
+notation "'le_to_eqm'" non associative with precedence 55 for @{'le_to_eqm}.
+notation "'lem'" non associative with precedence 55 for @{'lem}.
+notation "'join'" non associative with precedence 55 for @{'join}.
+notation "'join_refl'" non associative with precedence 55 for @{'join_refl}.
+notation "'join_comm'" non associative with precedence 55 for @{'join_comm}.
+notation "'join_assoc'" non associative with precedence 55 for @{'join_assoc}.
+notation "'strong_extj'" non associative with precedence 55 for @{'strong_extj}.
+notation "'le_to_eqj'" non associative with precedence 55 for @{'le_to_eqj}.
+notation "'lej'" non associative with precedence 55 for @{'lej}.
interpretation "Lattice meet" 'meet = (sl_meet (latt_mcarr ?)).
interpretation "Lattice meet_refl" 'meet_refl = (sl_meet_refl (latt_mcarr ?)).
interpretation "Lattice le_to_eqj" 'le_to_eqj = (sl_le_to_eqm (latt_jcarr ?)).
interpretation "Lattice lej" 'lej = (sl_lem (latt_jcarr ?)).
-notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}.
-notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}.
-notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}.
-notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}.
+notation "'feq_jl'" non associative with precedence 55 for @{'feq_jl}.
+notation "'feq_jr'" non associative with precedence 55 for @{'feq_jr}.
+notation "'feq_ml'" non associative with precedence 55 for @{'feq_ml}.
+notation "'feq_mr'" non associative with precedence 55 for @{'feq_mr}.
interpretation "Lattice feq_jl" 'feq_jl = (sl_feq_ml (latt_jcarr ?)).
interpretation "Lattice feq_jr" 'feq_jr = (sl_feq_mr (latt_jcarr ?)).
interpretation "Lattice feq_ml" 'feq_ml = (sl_feq_ml (latt_mcarr ?)).
(βk.(alpha k) is_strong_sup (shift ? xn k) in E) β§
x is_strong_inf alpha in E.
-notation < "x \nbsp 'is_limsup' \nbsp s" non associative with precedence 50 for @{'limsup $_ $s $x}.
-notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 50 for @{'liminf $_ $s $x}.
-notation > "x 'is_limsup' s 'in' e" non associative with precedence 50 for @{'limsup $e $s $x}.
-notation > "x 'is_liminf' s 'in' e" non associative with precedence 50 for @{'liminf $e $s $x}.
+notation < "x \nbsp 'is_limsup' \nbsp s" non associative with precedence 55 for @{'limsup $_ $s $x}.
+notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 55 for @{'liminf $_ $s $x}.
+notation > "x 'is_limsup' s 'in' e" non associative with precedence 55 for @{'limsup $e $s $x}.
+notation > "x 'is_liminf' s 'in' e" non associative with precedence 55 for @{'liminf $e $s $x}.
interpretation "Excess limsup" 'limsup e s x = (limsup e s x).
interpretation "Excess liminf" 'liminf e s x = (limsup (dual_exc e) s x).
definition lim β
Ξ»E:excess.Ξ»xn:sequence E.Ξ»x:E. x is_limsup xn in E β§ x is_liminf xn in E.
-notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 50 for @{'lim $_ $s $x}.
-notation > "x 'is_lim' s 'in' e" non associative with precedence 50 for @{'lim $e $s $x}.
+notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 55 for @{'lim $_ $s $x}.
+notation > "x 'is_lim' s 'in' e" non associative with precedence 55 for @{'lim $e $s $x}.
interpretation "Excess lim" 'lim e s x = (lim e s x).
lemma sup_decreasing:
definition d2s β
Ξ»R.Ξ»ms:metric_space R.Ξ»s:sequence ms.Ξ»k.Ξ»n. Ξ΄ (s n) k.
-notation "s β x" non associative with precedence 50 for @{'tends $s $x}.
+notation "s β x" non associative with precedence 55 for @{'tends $s $x}.
interpretation "tends to" 'tends s x = (tends0 ? (d2s ? ? s x)).
axiom leq: S β S β Prop.
-notation "hvbox(A break β B)" with precedence 59
+notation "hvbox(A break β B)" with precedence 64
for @{ 'subseteq $A $B}.
interpretation "Subseteq" 'subseteq A B = (leq A B).
axiom leq: S β S β Prop.
-notation "hvbox(A break β B)" with precedence 59
+notation "hvbox(A break β B)" with precedence 64
for @{ 'subseteq $A $B}.
interpretation "Subseteq" 'subseteq A B = (leq A B).
axiom eps: S.
axiom eps_idempotent: eps = eps eps.
-notation "hvbox(A break β B)" with precedence 59
+notation "hvbox(A break β B)" with precedence 64
for @{ 'subseteq $A $B}.
interpretation "Subseteq" 'subseteq A B = (eq ? A (comp eps B)).
record powerset (A : Type) : Type := { content : A β CProp }.
-notation > "Ξ© ^ A" non associative with precedence 50 for @{'P $A}.
-notation "Ξ© \sup A" non associative with precedence 50 for @{'P $A}.
+notation > "Ξ© ^ A" non associative with precedence 55 for @{'P $A}.
+notation "Ξ© \sup A" non associative with precedence 55 for @{'P $A}.
interpretation "Powerset" 'P A = (powerset A).
record AxiomSet : Type := {
definition in_subset :=
Ξ»A:AxiomSet.Ξ»aβA.Ξ»U:Ξ©^A.content A U a.
-notation "hvbox(a break Ξ΅U)" non associative with precedence 50 for
+notation "hvbox(a break Ξ΅U)" non associative with precedence 55 for
@{'in_subset $a $U}.
interpretation "In subset" 'in_subset a U = (in_subset ? a U).
(* NOTATION FOR THE "functional" COMPONENT ********************************)
notation "hvbox( β [ d , break e ] break T )"
- non associative with precedence 55
+ non associative with precedence 60
for @{ 'Lift $d $e $T }.
notation "hvbox( [ d β break V ] break T )"
- non associative with precedence 55
+ non associative with precedence 60
for @{ 'Subst $V $d $T }.
notation "hvbox( T1 β¨ break T2 )"
qed.
(* Basic_1: was: sn3_beta *)
-lemma csn_appl_beta: βL,W. L β’ β¬* W β βV,T. L β’ β¬* (βV. T) β (**)
+lemma csn_appl_beta: βL,W. L β’ β¬* W β βV,T. L β’ β¬* βV. T β
L β’ β¬* βV. βW. T.
/2 width=3/ qed.
(* Properties concerning basic local environment slicing ********************)
(* Basic_1: was: csubc_drop_conf_O *)
-(* Note: the constant (0) can not be generalized *)
+(* Note: the constant 0 can not be generalized *)
lemma lsubc_ldrop_O1_trans: βRP,L1,L2. L1 [RP] β L2 β βK2,e. β©[0, e] L2 β‘ K2 β
ββK1. β©[0, e] L1 β‘ K1 & K1 [RP] β K2.
#RP #L1 #L2 #H elim H -L1 -L2
non associative with precedence 90
for @{ 'GRef $p }.
-notation "hvbox( β‘ term 90 T1 . break term 90 T )"
- non associative with precedence 90
+notation "hvbox( β‘ term 55 T1 . break term 55 T )"
+ non associative with precedence 55
for @{ 'SnItem2 $T1 $T }.
-notation "hvbox( β‘ { I } break term 90 T1 . break term 90 T )"
- non associative with precedence 90
+notation "hvbox( β‘ { I } break term 55 T1 . break term 55 T )"
+ non associative with precedence 55
for @{ 'SnItem2 $I $T1 $T }.
-notation "hvbox( β { I } break term 90 T1 . break term 90 T )"
- non associative with precedence 90
+notation "hvbox( β { I } break term 55 T1 . break term 55 T )"
+ non associative with precedence 55
for @{ 'SnBind2 $I $T1 $T }.
-notation "hvbox( β { I } break term 90 T1 . break term 90 T )"
- non associative with precedence 90
+notation "hvbox( β { I } break term 55 T1 . break term 55 T )"
+ non associative with precedence 55
for @{ 'SnFlat2 $I $T1 $T }.
-notation "hvbox( β term 90 T1 . break term 90 T2 )"
- non associative with precedence 90
+notation "hvbox( β term 55 T1 . break term 55 T2 )"
+ non associative with precedence 55
for @{ 'SnAbbr $T1 $T2 }.
-notation "hvbox( β term 90 T1 . break term 90 T2 )"
- non associative with precedence 90
+notation "hvbox( β term 55 T1 . break term 55 T2 )"
+ non associative with precedence 55
for @{ 'SnAbst $T1 $T2 }.
-notation "hvbox( β term 90 T1 . break term 90 T2 )"
- non associative with precedence 90
+notation "hvbox( β term 55 T1 . break term 55 T2 )"
+ non associative with precedence 55
for @{ 'SnAppl $T1 $T2 }.
-notation "hvbox( β£ term 90 T1 . break term 90 T2 )"
- non associative with precedence 90
+notation "hvbox( β£ term 55 T1 . break term 55 T2 )"
+ non associative with precedence 55
for @{ 'SnCast $T1 $T2 }.
-notation "hvbox( βΆ term 90 T1 . break term 90 T )"
- non associative with precedence 90
+notation "hvbox( βΆ term 55 T1 . break term 55 T )"
+ non associative with precedence 55
for @{ 'SnApplV $T1 $T }.
notation > "hvbox( T . break β‘{ I } break term 47 T1 )"
non associative with precedence 46
for @{ 'DxBind2 $T $I $T1 }.
-notation "hvbox( T . break β { I } break term 90 T1 )"
- non associative with precedence 89
+notation "hvbox( T . break β { I } break term 48 T1 )"
+ non associative with precedence 47
for @{ 'DxBind2 $T $I $T1 }.
notation "hvbox( T1 . break β T2 )"
for @{ 'DxAbst $T1 $T2 }.
notation "hvbox( T . break β£ { I } break { T1 , break T2 , break T3 } )"
- non associative with precedence 47
+ non associative with precedence 50
for @{ 'DxItem4 $T $I $T1 $T2 $T3 }.
notation "hvbox( # [ x ] )"
non associative with precedence 45
for @{ 'Simple $T }.
-notation "hvbox( L β’ break term 90 T1 β break T2 )"
+notation "hvbox( L β’ break term 46 T1 β break term 46 T2 )"
non associative with precedence 45
for @{ 'Hom $L $T1 $T2 }.
-notation "hvbox( T1 β break T2 )"
+notation "hvbox( T1 β break term 46 T2 )"
non associative with precedence 45
for @{ 'Iso $T1 $T2 }.
-notation "hvbox( T1 break [ d , break e ] βΌ break T2 )"
+notation "hvbox( T1 break [ d , break e ] βΌ break term 46 T2 )"
non associative with precedence 45
for @{ 'SubEq $T1 $d $e $T2 }.
non associative with precedence 45
for @{ 'Normal $L $d $e $T }.
-notation "hvbox( β§ [ d , break e ] break T1 β‘ break T2 )"
+notation "hvbox( β§ [ d , break e ] break term 46 T1 β‘ break term 46 T2 )"
non associative with precedence 45
for @{ 'RLift $d $e $T1 $T2 }.
-notation "hvbox( β© [ e ] break L1 β‘ break L2 )"
+notation "hvbox( β© [ e ] break term 46 L1 β‘ break term 46 L2 )"
non associative with precedence 45
for @{ 'RDrop $e $L1 $L2 }.
-notation "hvbox( β© [ d , break e ] break L1 β‘ break L2 )"
+notation "hvbox( β© [ d , break e ] break term 46 L1 β‘ break term 46 L2 )"
non associative with precedence 45
for @{ 'RDrop $d $e $L1 $L2 }.
-notation "hvbox( L β’ break β [ T ] β‘ break k )"
+notation "hvbox( L β’ break β [ T ] β‘ break term 46 k )"
non associative with precedence 45
for @{ 'ICM $L $T $k }.
-notation "hvbox( L β’ break term 90 T1 break [ d , break e ] βΆ break T2 )"
+notation "hvbox( L β’ break term 46 T1 break [ d , break e ] βΆ break term 46 T2 )"
non associative with precedence 45
for @{ 'PSubst $L $T1 $d $e $T2 }.
(* Unfold *******************************************************************)
-notation "hvbox( @ [ T1 ] break f β‘ break T2 )"
+notation "hvbox( @ [ T1 ] break term 46 f β‘ break term 46 T2 )"
non associative with precedence 45
for @{ 'RAt $T1 $f $T2 }.
-notation "hvbox( T1 β break T2 β‘ break T )"
+notation "hvbox( T1 β break term 46 T2 β‘ break term 46 T )"
non associative with precedence 45
for @{ 'RMinus $T1 $T2 $T }.
-notation "hvbox( β§ * [ e ] break T1 β‘ break T2 )"
+notation "hvbox( β§ * [ e ] break term 46 T1 β‘ break term 46 T2 )"
non associative with precedence 45
for @{ 'RLiftStar $e $T1 $T2 }.
-notation "hvbox( β© * [ e ] break L1 β‘ break L2 )"
+notation "hvbox( β© * [ e ] break term 46 L1 β‘ break term 46 L2 )"
non associative with precedence 45
for @{ 'RDropStar $e $L1 $L2 }.
-notation "hvbox( T1 break [ d , break e ] βΆ* break T2 )"
+notation "hvbox( T1 break [ d , break e ] βΆ* break term 46 T2 )"
non associative with precedence 45
for @{ 'PSubstStar $T1 $d $e $T2 }.
-notation "hvbox( L β’ break term 90 T1 break [ d , break e ] βΆ* break T2 )"
+notation "hvbox( L β’ break term 46 T1 break [ d , break e ] βΆ* break term 46 T2 )"
non associative with precedence 45
for @{ 'PSubstStar $L $T1 $d $e $T2 }.
-notation "hvbox( L β’ break term 90 T1 break [ d , break e ] βΆβΆ* break T2 )"
+notation "hvbox( L β’ break term 46 T1 break [ d , break e ] βΆβΆ* break term 46 T2 )"
non associative with precedence 45
for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
-notation "hvbox( T1 break [ d , break e ] β‘ break T2 )"
+notation "hvbox( T1 break [ d , break e ] β‘ break term 46 T2 )"
non associative with precedence 45
for @{ 'TSubst $T1 $d $e $T2 }.
-notation "hvbox( L β’ break term 90 T1 break [ d , break e ] β‘ break T2 )"
+notation "hvbox( L β’ break term 46 T1 break [ d , break e ] β‘ break term 46 T2 )"
non associative with precedence 45
for @{ 'TSubst $L $T1 $d $e $T2 }.
non associative with precedence 45
for @{ 'TSubstAlt $T1 $d $e $T2 }.
-notation "hvbox( L β’ break term 90 T1 break [ d , break e ] β‘β‘ break term 46 T2 )"
+notation "hvbox( L β’ break term 46 T1 break [ d , break e ] β‘β‘ break term 46 T2 )"
non associative with precedence 45
for @{ 'TSubstAlt $L $T1 $d $e $T2 }.
(* Static typing ************************************************************)
-notation "hvbox( L β’ break term 90 T Γ· break A )"
+notation "hvbox( L β’ break term 46 T Γ· break term 46 A )"
non associative with precedence 45
for @{ 'AtomicArity $L $T $A }.
-notation "hvbox( T1 Γ· β break T2 )"
+notation "hvbox( T1 Γ· β break term 46 T2 )"
non associative with precedence 45
for @{ 'CrSubEqA $T1 $T2 }.
-notation "hvbox( β¦ h , break L β¦ β’ break term 90 T1 β’ break T2 )"
+notation "hvbox( β¦ h , break L β¦ β’ break term 46 T1 β’ break term 46 T2 )"
non associative with precedence 45
for @{ 'StaticType $h $L $T1 $T2 }.
(* Unwind *******************************************************************)
-notation "hvbox( β¦ h , break L β¦ β’ break term 90 T1 β’* break T2 )"
+notation "hvbox( β¦ h , break L β¦ β’ break term 46 T1 β’* break term 46 T2 )"
non associative with precedence 45
for @{ 'StaticTypeStar $h $L $T1 $T2 }.
non associative with precedence 45
for @{ 'WHdNormal $L $T }.
-notation "hvbox( T1 β‘ break T2 )"
+notation "hvbox( T1 β‘ break term 46 T2 )"
non associative with precedence 45
for @{ 'PRed $T1 $T2 }.
-notation "hvbox( L β’ break term 90 T1 β‘ break T2 )"
+notation "hvbox( L β’ break term 46 T1 β‘ break term 46 T2 )"
non associative with precedence 45
for @{ 'PRed $L $T1 $T2 }.
-notation "hvbox( L1 β’ β‘ break L2 )"
+notation "hvbox( L1 β’ β‘ break term 46 L2 )"
non associative with precedence 45
for @{ 'CPRed $L1 $L2 }.
(* Computation **************************************************************)
-notation "hvbox( T1 β‘* break T2 )"
+notation "hvbox( T1 β‘* break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedStar $T1 $T2 }.
-notation "hvbox( L β’ break term 90 T1 β‘* break T2 )"
+notation "hvbox( L β’ break term 46 T1 β‘* break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedStar $L $T1 $T2 }.
-notation "hvbox( L1 β’ β‘* break L2 )"
+notation "hvbox( L1 β’ β‘* break term 46 L2 )"
non associative with precedence 45
for @{ 'CPRedStar $L1 $L2 }.
-notation "hvbox( L β’ break term 90 T1 β‘* break π [ T2 ] )"
+notation "hvbox( L β’ break term 46 T1 β‘* break π [ T2 ] )"
non associative with precedence 45
for @{ 'PEval $L $T1 $T2 }.
-notation "hvbox( β¬ * T )"
+notation "hvbox( β¬ * term 46 T )"
non associative with precedence 45
for @{ 'SN $T }.
-notation "hvbox( L β’ β¬ * T )"
+notation "hvbox( L β’ β¬ * term 46 T )"
non associative with precedence 45
for @{ 'SN $L $T }.
-notation "hvbox( L β’ β¬ * * T )"
+notation "hvbox( L β’ β¬ * * term 46 T )"
non associative with precedence 45
for @{ 'SNStar $L $T }.
non associative with precedence 45
for @{ 'InEInt $R $L $T $A }.
-notation "hvbox( T1 break [ R ] β break T2 )"
+notation "hvbox( T1 break [ R ] β break term 46 T2 )"
non associative with precedence 45
for @{ 'CrSubEq $T1 $R $T2 }.
(* Conversion ***************************************************************)
-notation "hvbox( L β’ break term 90 T1 β¬ break T2 )"
+notation "hvbox( L β’ break term 46 T1 β¬ break term 46 T2 )"
non associative with precedence 45
for @{ 'PConv $L $T1 $T2 }.
-notation "hvbox( T1 β’ β¬ break T2 )"
+notation "hvbox( T1 β’ β¬ break term 46 T2 )"
non associative with precedence 45
for @{ 'CPConv $T1 $T2 }.
(* Equivalence **************************************************************)
-notation "hvbox( L β’ break term 90 T1 β¬* break T2 )"
+notation "hvbox( L β’ break term 46 T1 β¬* break term 46 T2 )"
non associative with precedence 45
for @{ 'PConvStar $L $T1 $T2 }.
-notation "hvbox( T1 β’ β¬* break T2 )"
+notation "hvbox( T1 β’ β¬* break term 46 T2 )"
non associative with precedence 45
for @{ 'CPConvStar $T1 $T2 }.
(* Dynamic typing ***********************************************************)
-notation "hvbox( β¦ h , break L β¦ β’ break term 90 T1 : break T2 )"
+notation "hvbox( β¦ h , break L β¦ β’ break term 46 T1 : break term 46 T2 )"
non associative with precedence 45
for @{ 'NativeType $h $L $T1 $T2 }.
-notation "hvbox( h β’ break term 90 L1 : β break L2 )"
+notation "hvbox( h β’ break term 46 L1 : β break term 46 L2 )"
non associative with precedence 45
for @{ 'CrSubEqN $h $L1 $L2 }.
| ltpss_pair : βL,I,V. ltpss 0 0 (L. β{I} V) (L. β{I} V)
| ltpss_tpss2: βL1,L2,I,V1,V2,e.
ltpss 0 e L1 L2 β L2 β’ V1 [0, e] βΆ* V2 β
- ltpss 0 (e + 1) (L1. β{I} V1) L2. β{I} V2
+ ltpss 0 (e + 1) (L1. β{I} V1) (L2. β{I} V2)
| ltpss_tpss1: βL1,L2,I,V1,V2,d,e.
ltpss d e L1 L2 β L2 β’ V1 [d, e] βΆ* V2 β
ltpss (d + 1) e (L1. β{I} V1) (L2. β{I} V2)
for @{'bigop ($b-$a) $op $nil (Ξ»${ident j}.((Ξ»${ident j}.true) (${ident j}+$a)))
(Ξ»${ident j}.((Ξ»${ident j}.$f)(${ident j}+$a)))}.
-(* notation "\big [ op , nil ]_{( term 50) a β€ ident j < b | p } f"
+(* notation "\big [ op , nil ]_{( term 55) a β€ ident j < b | p } f"
with precedence 80
for @{\big[$op,$nil]_{${ident j} < ($b-$a) | ((Ξ»${ident j}.$p) (${ident j}+$a))}((Ξ»${ident j}.$f)(${ident j}+$a))}.
*)
for @{ 'ndivides $a $b }.
notation "hvbox(a break + b)"
- left associative with precedence 50
+ left associative with precedence 55
for @{ 'plus $a $b }.
notation "hvbox(a break - b)"
- left associative with precedence 50
+ left associative with precedence 55
for @{ 'minus $a $b }.
notation "hvbox(a break * b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'times $a $b }.
notation "hvbox(a break \middot b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'middot $a $b }.
notation "hvbox(a break \mod b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'module $a $b }.
notation < "a \frac b"
for @{ 'divide $a $b }.
notation "a \over b"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'divide $a $b }.
notation "hvbox(a break / b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'divide $a $b }.
-notation "- term 60 a" with precedence 60
+notation "- term 65 a" with precedence 65
for @{ 'uminus $a }.
notation "a !"
for @{ 'fact $a }.
notation "\sqrt a"
- non associative with precedence 60
+ non associative with precedence 65
for @{ 'sqrt $a }.
notation "hvbox(a break \lor b)"
notation "hvbox(a break β b)" non associative with precedence 45
for @{ 'subseteq $a $b }. (* \subseteq *)
-notation "hvbox(a break β© b)" left associative with precedence 55
+notation "hvbox(a break β© b)" left associative with precedence 60
for @{ 'intersects $a $b }. (* \cap *)
-notation "hvbox(a break βͺ b)" left associative with precedence 50
+notation "hvbox(a break βͺ b)" left associative with precedence 55
for @{ 'union $a $b }. (* \cup *)
notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
for @{ 'apart $a $b}.
notation "hvbox(a break \circ b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'compose $a $b }.
-notation < "β \ensp a" with precedence 55 for @{ 'downarrow $a }.
-notation > "β a" with precedence 55 for @{ 'downarrow $a }.
+notation < "β \ensp a" with precedence 60 for @{ 'downarrow $a }.
+notation > "β a" with precedence 60 for @{ 'downarrow $a }.
-notation "hvbox(U break β V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
+notation "hvbox(U break β V)" non associative with precedence 60 for @{ 'fintersects $U $V }.
-notation "βa" with precedence 55 for @{ 'uparrow $a }.
+notation "βa" with precedence 60 for @{ 'uparrow $a }.
-notation "hvbox(a break β b)" with precedence 55 for @{ 'funion $a $b }.
+notation "hvbox(a break β b)" with precedence 60 for @{ 'funion $a $b }.
notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
notation > "x β© y" with precedence 45 for @{'Vdash2 $x $y ?}.
notation > "x β©β½ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
notation "x (β© \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
-notation > "β© " with precedence 60 for @{'Vdash ?}.
-notation "(β© \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
+notation > "β© " with precedence 65 for @{'Vdash ?}.
+notation "(β© \sub term 90 c) " with precedence 65 for @{'Vdash $c}.
notation < "maction (mstyle color #ff0000 (Ββ¦Β)) (t)"
non associative with precedence 90 for @{'hide $t}.
[ nil β 0
| cons a tl β S (length A tl)].
-notation "|M|" non associative with precedence 60 for @{'norm $M}.
+notation "|M|" non associative with precedence 65 for @{'norm $M}.
interpretation "norm" 'norm l = (length ? l).
lemma length_tail: βA,l. length ? (tail A l) = pred (length ? l).
FP: map_objs2 ?? F F1 =_\ID F2
}.
-notation "β±\sub 1 x" non associative with precedence 60 for @{'F1 $x}.
+notation "β±\sub 1 x" non associative with precedence 65 for @{'F1 $x}.
notation > "β±_1" non associative with precedence 90 for @{F1 ???}.
interpretation "F1" 'F1 x = (F1 ??? x).
-notation "β±\sub 2 x" non associative with precedence 60 for @{'F2 $x}.
+notation "β±\sub 2 x" non associative with precedence 65 for @{'F2 $x}.
notation > "β±_2" non associative with precedence 90 for @{F2 ???}.
interpretation "F2" 'F2 x = (F2 ??? x).
FmP: REW ?? F X Y (map_arrows2 ?? F ?? Fm1) = Fm2
}.
-notation "β³\sub 1 x" non associative with precedence 60 for @{'Fm1 $x}.
+notation "β³\sub 1 x" non associative with precedence 65 for @{'Fm1 $x}.
notation > "β³_1" non associative with precedence 90 for @{Fm1 ?????}.
interpretation "Fm1" 'Fm1 x = (Fm1 ????? x).
-notation "β³\sub 2 x" non associative with precedence 60 for @{'Fm2 $x}.
+notation "β³\sub 2 x" non associative with precedence 65 for @{'Fm2 $x}.
notation > "β³_2" non associative with precedence 90 for @{Fm2 ?????}.
interpretation "Fm2" 'Fm2 x = (Fm2 ????? x).
interpretation "setoid2 symmetry" 'invert r = (sym2 ???? r).
interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r).
interpretation "setoid symmetry" 'invert r = (sym ???? r).
-notation ".= r" with precedence 50 for @{'trans $r}.
+notation ".= r" with precedence 55 for @{'trans $r}.
interpretation "trans3" 'trans r = (trans3 ????? r).
interpretation "trans2" 'trans r = (trans2 ????? r).
interpretation "trans1" 'trans r = (trans1 ????? r).
#A #B #e #b @(fi ?? e) assumption.
qed.
-notation ". r" with precedence 50 for @{'fi $r}.
+notation ". r" with precedence 55 for @{'fi $r}.
interpretation "fi" 'fi r = (fi' ?? r).
definition and_morphism: binary_morphism1 CPROP CPROP CPROP.
| @(fi ?? e1) @f @(if ?? e) assumption]]
qed.
(*
-notation > "hvbox(a break β b)" left associative with precedence 55 for @{ comp ??? $a $b }.
+notation > "hvbox(a break β b)" left associative with precedence 60 for @{ comp ??? $a $b }.
*)
record category : Type[1] β {
objs:> Type[0];
id_neutral_right: βo1,o2. βa: arrows o1 o2. comp ??? a (id o2) =_0 a
}.
(*
-notation "hvbox(a break β b)" left associative with precedence 55 for @{ 'compose $a $b }.
+notation "hvbox(a break β b)" left associative with precedence 60 for @{ 'compose $a $b }.
*)
record category1 : Type[2] β
{ objs1:> Type[1];
βo1,o2,o3.βf1:arrows2 ? o1 o2.βf2:arrows2 ? o2 o3.
map_arrows2 ?? (f2 β f1) = map_arrows2 ?? f2 β map_arrows2 ?? f1}.
-notation > "Fβ½β x" left associative with precedence 60 for @{'map_arrows2 $F $x}.
-notation "F\subβ x" left associative with precedence 60 for @{'map_arrows2 $F $x}.
+notation > "Fβ½β x" left associative with precedence 65 for @{'map_arrows2 $F $x}.
+notation "F\subβ x" left associative with precedence 65 for @{'map_arrows2 $F $x}.
interpretation "map_arrows2" 'map_arrows2 F x = (fun12 ?? (map_arrows2 ?? F ??) x).
definition functor2_setoid: category2 β category2 β setoid3.
interpretation "o-algebra overlap" 'overlap a b = (fun21 ??? (oa_overlap ?) a b).
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (β§) \below (\emsp) \nbsp term 90 p)"
-non associative with precedence 50 for @{ 'oa_meet $p }.
+non associative with precedence 55 for @{ 'oa_meet $p }.
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (β§) \below (ident i β βI) break term 90 p)"
-non associative with precedence 50 for @{ 'oa_meet_mk (Ξ»${ident i}:$I.$p) }.
+non associative with precedence 55 for @{ 'oa_meet_mk (Ξ»${ident i}:$I.$p) }.
-notation > "hovbox(β§ f)" non associative with precedence 60
+notation > "hovbox(β§ f)" non associative with precedence 65
for @{ 'oa_meet $f }.
interpretation "o-algebra meet" 'oa_meet f =
(fun12 ?? (oa_meet ??) f).
(fun12 ?? (oa_meet ??) (mk_unary_morphism1 ?? f ?)).
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (β¨) \below (\emsp) \nbsp term 90 p)"
-non associative with precedence 50 for @{ 'oa_join $p }.
+non associative with precedence 55 for @{ 'oa_join $p }.
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (β¨) \below (ident i β βI) break term 90 p)"
-non associative with precedence 50 for @{ 'oa_join_mk (Ξ»${ident i}:$I.$p) }.
+non associative with precedence 55 for @{ 'oa_join_mk (Ξ»${ident i}:$I.$p) }.
-notation > "hovbox(β¨ f)" non associative with precedence 60
+notation > "hovbox(β¨ f)" non associative with precedence 65
for @{ 'oa_join $f }.
interpretation "o-algebra join" 'oa_join f =
(fun12 ?? (oa_join ??) f).
notation < "hovbox(a β¨ b)" left associative with precedence 49
for @{ 'oa_join_mk (Ξ»${ident i}:$_.match $i with [ true β $a | false β $b ]) }.
-notation > "hovbox(β¨ f)" non associative with precedence 59
+notation > "hovbox(β¨ f)" non associative with precedence 64
for @{ 'oa_join $f }.
notation > "hovbox(a β¨ b)" left associative with precedence 49
for @{ 'oa_join (mk_unary_morphism BOOL ? (Ξ»x__:bool.match x__ with [ true β $a | false β $b ]) (IF_THEN_ELSE_p ? $a $b)) }.
| intros; apply (#β‘e); ]
qed.
-notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
+notation < "F x" left associative with precedence 65 for @{'map_arrows $F $x}.
interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x).
definition preserve_sup : βS,T.β f:Ξ©^S β_1 Ξ©^T. CProp[1].
qed.
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (β) \below (\emsp) term 90 p)"
-non associative with precedence 50 for @{ 'bigcup $p }.
+non associative with precedence 55 for @{ 'bigcup $p }.
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (β) \below (ident i β βI) break term 90 p)"
-non associative with precedence 50 for @{ 'bigcup_mk (Ξ»${ident i}:$I.$p) }.
-notation > "hovbox(β f)" non associative with precedence 60 for @{ 'bigcup $f }.
+non associative with precedence 55 for @{ 'bigcup_mk (Ξ»${ident i}:$I.$p) }.
+notation > "hovbox(β f)" non associative with precedence 65 for @{ 'bigcup $f }.
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (β) \below (\emsp) term 90 p)"
-non associative with precedence 50 for @{ 'bigcap $p }.
+non associative with precedence 55 for @{ 'bigcap $p }.
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (β) \below (ident i β βI) break term 90 p)"
-non associative with precedence 50 for @{ 'bigcap_mk (Ξ»${ident i}:$I.$p) }.
-notation > "hovbox(β f)" non associative with precedence 60 for @{ 'bigcap $f }.
+non associative with precedence 55 for @{ 'bigcap_mk (Ξ»${ident i}:$I.$p) }.
+notation > "hovbox(β f)" non associative with precedence 65 for @{ 'bigcap $f }.
interpretation "bigcup" 'bigcup f = (fun12 ?? (big_union ??) f).
interpretation "bigcap" 'bigcap f = (fun12 ?? (big_intersects ??) f).
non associative with precedence 45
for @{'Eq1 $c $a $b}.
-notation "hbox(! term 50 a)"
- non associative with precedence 50
+notation "hbox(! term 55 a)"
+ non associative with precedence 55
for @{'Invariant $a}.
-notation "hbox((! ^ term 90 b) term 50 a)"
- non associative with precedence 50
+notation "hbox((! ^ term 90 b) term 55 a)"
+ non associative with precedence 55
for @{'Invariant1 $a $b}.
(* lifting, substitution *)
notation "hvbox(β [ p break , k ] break t)"
- non associative with precedence 50
+ non associative with precedence 55
for @{'Lift1 $p $k $t}.
notation "hvbox(M break [ / l ])"
(* interpretations *)
notation "hvbox(βTβ)"
- non associative with precedence 50
+ non associative with precedence 55
for @{'IInt $T}.
notation "hvbox(βTβ break _ [E])"
- non associative with precedence 50
+ non associative with precedence 55
for @{'IInt1 $T $E}.
notation "hvbox(βTβ break _ [E1 break , E2])"
- non associative with precedence 50
+ non associative with precedence 55
for @{'IInt2 $T $E1 $E2}.
notation "hvbox(βTβ * break _ [E])"
- non associative with precedence 50
+ non associative with precedence 55
for @{'IIntS1 $T $E}.
notation "hvbox(γTγ)"
- non associative with precedence 50
+ non associative with precedence 55
for @{'EInt $T}.
notation "hvbox(γTγ break _ [E])"
- non associative with precedence 50
+ non associative with precedence 55
for @{'EInt1 $T $E}.
notation "hvbox(γTγ break _ [E1 break , E2])"
- non associative with precedence 50
+ non associative with precedence 55
for @{'EInt2 $T $E1 $E2}.
notation "hvbox(γTγ)"
- non associative with precedence 50
+ non associative with precedence 55
for @{'XInt $T}.
notation "hvbox(γTγ break _ [E])"
- non associative with precedence 50
+ non associative with precedence 55
for @{'XInt1 $T $E}.
notation "hvbox(γTγ break _ [E1 break , E2])"
- non associative with precedence 50
+ non associative with precedence 55
for @{'XInt2 $T $E1 $E2}.
notation "hvbox(π{G})"
- non associative with precedence 50
+ non associative with precedence 55
for @{'IK $G}.
notation "hvbox(π{T} break _ [G])"
- non associative with precedence 50
+ non associative with precedence 55
for @{'IK $T $G}.
non associative with precedence 45
for @{'Eq1 $c $a $b}.
-notation "hbox(! term 50 a)"
- non associative with precedence 50
+notation "hbox(! term 55 a)"
+ non associative with precedence 55
for @{'Invariant $a}.
-notation "hbox((! ^ term 90 b) term 50 a)"
- non associative with precedence 50
+notation "hbox((! ^ term 90 b) term 55 a)"
+ non associative with precedence 55
for @{'Invariant1 $a $b}.
(* lifting, substitution *)
notation "hvbox(β [ p break , k ] break t)"
- non associative with precedence 50
+ non associative with precedence 55
for @{'Lift1 $p $k $t}.
notation "hvbox(M break [ / l ])"
(* interpretations *)
notation "hvbox(βTβ)"
- non associative with precedence 50
+ non associative with precedence 55
for @{'IInt $T}.
notation "hvbox(βTβ break _ [E])"
- non associative with precedence 50
+ non associative with precedence 55
for @{'IInt1 $T $E}.
notation "hvbox(βTβ break _ [E1 break , E2])"
- non associative with precedence 50
+ non associative with precedence 55
for @{'IInt2 $T $E1 $E2}.
notation "hvbox(γTγ)"
- non associative with precedence 50
+ non associative with precedence 55
for @{'EInt $T}.
notation "hvbox(γTγ break _ [E])"
- non associative with precedence 50
+ non associative with precedence 55
for @{'EInt1 $T $E}.
notation "hvbox(γTγ break _ [E1 break , E2])"
- non associative with precedence 50
+ non associative with precedence 55
for @{'EInt2 $T $E1 $E2}.
notation "hvbox(γTγ)"
- non associative with precedence 50
+ non associative with precedence 55
for @{'XInt $T}.
notation "hvbox(γTγ break _ [E])"
- non associative with precedence 50
+ non associative with precedence 55
for @{'XInt1 $T $E}.
notation "hvbox(γTγ break _ [E1 break , E2])"
- non associative with precedence 50
+ non associative with precedence 55
for @{'XInt2 $T $E1 $E2}.
(* concatenation *)
definition cat : βS,l1,l2,w.Prop β
Ξ»S.Ξ»l1,l2.Ξ»w:word S.βw1,w2.w1 @ w2 = w β§ l1 w1 β§ l2 w2.
-notation "a Β· b" non associative with precedence 60 for @{ 'middot $a $b}.
+notation "a Β· b" non associative with precedence 65 for @{ 'middot $a $b}.
interpretation "cat lang" 'middot a b = (cat ? a b).
let rec flatten (S : DeqSet) (l : list (word S)) on l : word S β
]
qed.
-notation > "x β¦* E" non associative with precedence 60 for @{moves ? $x $E}.
+notation > "x β¦* E" non associative with precedence 65 for @{moves ? $x $E}.
let rec moves (S : DeqSet) w e on w : pre S β
match w with
[ nil β e
*)
definition lo β Ξ»S:DeqSet.Ξ»a,b:pre S.β©\fst a + \fst b,\snd a β¨ \snd bβͺ.
-notation "a β b" left associative with precedence 60 for @{'oplus $a $b}.
+notation "a β b" left associative with precedence 65 for @{'oplus $a $b}.
interpretation "oplus" 'oplus a b = (lo ? a b).
lemma lo_def: βS.βi1,i2:pitem S.βb1,b2. β©i1,b1βͺββ©i2,b2βͺ=β©i1+i2,b1β¨b2βͺ.
definition pre_concat_r β Ξ»S:DeqSet.Ξ»i:pitem S.Ξ»e:pre S.
match e with [ mk_Prod i1 b β β©i Β· i1, bβͺ].
-notation "i β e" left associative with precedence 60 for @{'lhd $i $e}.
+notation "i β e" left associative with precedence 65 for @{'lhd $i $e}.
interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
(* The behaviour of β is summarized by the following, easy lemma: *)
]
].
-notation "a βΉ b" left associative with precedence 60 for @{'tril eclose $a $b}.
+notation "a βΉ b" left associative with precedence 65 for @{'tril eclose $a $b}.
interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
-notation "β’" non associative with precedence 60 for @{eclose ?}.
+notation "β’" non associative with precedence 65 for @{eclose ?}.
(* We are ready to give the formal definition of the broadcasting operation. *)
| pc i1 i2 β β’i1 βΉ i2
| pk i β β©(\fst (β’i))^*,trueβͺ].
-notation "β’ x" non associative with precedence 60 for @{'eclose $x}.
+notation "β’ x" non associative with precedence 65 for @{'eclose $x}.
interpretation "eclose" 'eclose x = (eclose ? x).
(* Here are a few simple properties of βΉ and β’(-) *)
interpretation "star" 'pk a = (k ? a).
interpretation "or" 'plus a b = (o ? a b).
-notation "a Β· b" non associative with precedence 60 for @{ 'pc $a $b}.
+notation "a Β· b" non associative with precedence 65 for @{ 'pc $a $b}.
interpretation "cat" 'pc a b = (c ? a b).
(* to get rid of \middot
interpretation "pepsilon" 'epsilon = (pe ?).
interpretation "pempty" 'empty = (pz ?).
-notation > "| e |" non associative with precedence 65 for @{forget ? $e}.
+notation > "| e |" non associative with precedence 66 for @{forget ? $e}.
let rec forget (S: Alpha) (l : pitem S) on l: re S β
match l with
[ pz β β
qed.
definition lo β Ξ»S:Alpha.Ξ»a,b:pre S.β©\fst a + \fst b,\snd a || \snd bβͺ.
-notation "a β b" left associative with precedence 60 for @{'oplus $a $b}.
+notation "a β b" left associative with precedence 65 for @{'oplus $a $b}.
interpretation "oplus" 'oplus a b = (lo ? a b).
lemma lo_def: βS.βi1,i2:pitem S.βb1,b2. β©i1,b1βͺββ©i2,b2βͺ=β©i1+i2,b1||b2βͺ.
match e with
[ pair i b β β©\fst (f S i), \snd (f S i) || bβͺ].
-notation < "a β b" left associative with precedence 60 for @{'lc $op $a $b}.
+notation < "a β b" left associative with precedence 65 for @{'lc $op $a $b}.
interpretation "lc" 'lc op a b = (lc ? op a b).
-notation > "a β b" left associative with precedence 60 for @{'lc (lift eclose) $a $b}.
+notation > "a β b" left associative with precedence 65 for @{'lc (lift eclose) $a $b}.
definition lk β Ξ»S:Alpha.Ξ»bcast:βS:Alpha.βE:pitem S.pre S.Ξ»e:pre S.
match e with
notation > "a^β" non associative with precedence 90 for @{'lk eclose $a}.
-notation > "β’" non associative with precedence 60 for @{eclose ?}.
+notation > "β’" non associative with precedence 65 for @{eclose ?}.
let rec eclose (S: Alpha) (i: pitem S) on i : pre S β
match i with
[ pz β β© β
, false βͺ
| pc E1 E2 β β’E1 β β©E2,falseβͺ
| pk E β β©(\fst(β’E))^*,trueβͺ].
-notation < "β’ x" non associative with precedence 60 for @{'eclose $x}.
+notation < "β’ x" non associative with precedence 65 for @{'eclose $x}.
interpretation "eclose" 'eclose x = (eclose ? x).
-notation > "β’ x" non associative with precedence 60 for @{'eclose $x}.
+notation > "β’ x" non associative with precedence 65 for @{'eclose $x}.
definition reclose β lift eclose.
interpretation "reclose" 'eclose x = (reclose ? x).
STOP
notation > "\move term 90 x term 90 E"
-non associative with precedence 60 for @{move ? $x $E}.
+non associative with precedence 65 for @{move ? $x $E}.
nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S β
match E with
[ pz β β© β
, false βͺ
| po e1 e2 β \move x e1 β \move x e2
| pc e1 e2 β \move x e1 β \move x e2
| pk e β (\move x e)^β ].
-notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}.
-notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}.
+notation < "\move\shy x\shy E" non associative with precedence 65 for @{'move $x $E}.
+notation > "\move term 90 x term 90 E" non associative with precedence 65 for @{'move $x $E}.
interpretation "move" 'move x E = (move ? x E).
ndefinition rmove β Ξ»S:Alpha.Ξ»x:S.Ξ»e:pre S. \move x (\fst e).
nqed.
-notation > "x β¦* E" non associative with precedence 60 for @{move_star ? $x $E}.
+notation > "x β¦* E" non associative with precedence 65 for @{move_star ? $x $E}.
nlet rec move_star (S : decidable) w E on w : bool Γ (pre S) β
match w with
[ nil β E
interpretation "Finite_enumerable representation" 'repr S i =
(repr S (is_finite_enumerable S) i).
-notation "hvbox(\iota e)" with precedence 60
+notation "hvbox(\iota e)" with precedence 65
for @{ 'index_of_finite_enumerable_semigroup $e }.
interpretation "Index_of_finite_enumerable representation"
lemma eq_trans:βE:bishop_set.βx,z,y:E.x β y β y β z β x β z β
Ξ»E,x,y,z.eq_trans_ E x z y.
-notation > "'Eq'β" non associative with precedence 50
+notation > "'Eq'β" non associative with precedence 55
for @{'eqrewrite}.
interpretation "eq_rew" 'eqrewrite = (eq_trans ? ? ?).
intro Xyz; apply Exy; left; assumption;
qed.
-notation > "'Le'βͺ" non associative with precedence 50 for @{'lerewritel}.
+notation > "'Le'βͺ" non associative with precedence 55 for @{'lerewritel}.
interpretation "le_rewl" 'lerewritel = (le_rewl ? ? ?).
-notation > "'Le'β«" non associative with precedence 50 for @{'lerewriter}.
+notation > "'Le'β«" non associative with precedence 55 for @{'lerewriter}.
interpretation "le_rewr" 'lerewriter = (le_rewr ? ? ?).
lemma ap_rewl: βA:bishop_set.βx,z,y:A. x β y β y # z β x # z.
apply bs_symmetric; assumption;
qed.
-notation > "'Ap'βͺ" non associative with precedence 50 for @{'aprewritel}.
+notation > "'Ap'βͺ" non associative with precedence 55 for @{'aprewritel}.
interpretation "ap_rewl" 'aprewritel = (ap_rewl ? ? ?).
-notation > "'Ap'β«" non associative with precedence 50 for @{'aprewriter}.
+notation > "'Ap'β«" non associative with precedence 55 for @{'aprewriter}.
interpretation "ap_rewr" 'aprewriter = (ap_rewr ? ? ?).
lemma exc_rewl: βA:ordered_set.βx,z,y:A. x β y β y β° z β x β° z.
cases (Exy); left; assumption;
qed.
-notation > "'Ex'βͺ" non associative with precedence 50 for @{'ordered_setrewritel}.
+notation > "'Ex'βͺ" non associative with precedence 55 for @{'ordered_setrewritel}.
interpretation "exc_rewl" 'ordered_setrewritel = (exc_rewl ? ? ?).
-notation > "'Ex'β«" non associative with precedence 50 for @{'ordered_setrewriter}.
+notation > "'Ex'β«" non associative with precedence 55 for @{'ordered_setrewriter}.
interpretation "exc_rewr" 'ordered_setrewriter = (exc_rewr ? ? ?).
(*
[apply (Leβͺ ? (eq_sym ??? E));| apply (Apβͺ ? E);] assumption;
qed.
-notation > "'Lt'βͺ" non associative with precedence 50 for @{'ltrewritel}.
+notation > "'Lt'βͺ" non associative with precedence 55 for @{'ltrewritel}.
interpretation "lt_rewl" 'ltrewritel = (lt_rewl ? ? ?).
-notation > "'Lt'β«" non associative with precedence 50 for @{'ltrewriter}.
+notation > "'Lt'β«" non associative with precedence 55 for @{'ltrewriter}.
interpretation "lt_rewr" 'ltrewriter = (lt_rewr ? ? ?).
*)
definition hide β Ξ»T:Type.Ξ»x:T.x.
-notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
+notation < "\blacksquare" non associative with precedence 55 for @{'hide}.
interpretation "hide" 'hide = (hide ? ?).
interpretation "hide2" 'hide = (hide ? ? ?).
Ξ»C:bishop_set.Ξ»U:C squareB β Prop.
Ξ»x:C squareB. U β©\snd x,\fst xβͺ.
-notation > "\inv" with precedence 60 for @{ 'invert_symbol }.
+notation > "\inv" with precedence 65 for @{ 'invert_symbol }.
interpretation "relation invertion" 'invert a = (invert_bs_relation ? a).
interpretation "relation invertion" 'invert_symbol = (invert_bs_relation ?).
interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation ? a x).
interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y).
interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r).
interpretation "setoid symmetry" 'invert r = (sym ???? r).
-notation ".= r" with precedence 50 for @{'trans $r}.
+notation ".= r" with precedence 55 for @{'trans $r}.
interpretation "trans1" 'trans r = (trans1 ????? r).
interpretation "trans" 'trans r = (trans ????? r).
intros; apply (if ?? H); assumption.
qed.
-notation ". r" with precedence 50 for @{'if $r}.
+notation ". r" with precedence 55 for @{'if $r}.
interpretation "if" 'if r = (if' ?? r).
definition and_morphism: binary_morphism1 CPROP CPROP CPROP.
* Any file that includes this one can not use 'x' as an identifier
*)
notation "hvbox('X' \sup n)"
- non associative with precedence 60
+ non associative with precedence 65
for @{ 'monomio $n }.
notation "hvbox('X')"
- non associative with precedence 60
+ non associative with precedence 65
for @{ 'monomio 1 }.
interpretation "Rmonomio" 'monomio n = (monomio n).
*)
definition equiv β Ξ»F1,F2. βv.[[ F1 ]]v = [[ F2 ]]v.
notation "hvbox(a \nbsp break mstyle color #0000ff (β‘) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }.
-notation > "a β‘ b" non associative with precedence 50 for @{ equiv $a $b }.
+notation > "a β‘ b" non associative with precedence 55 for @{ equiv $a $b }.
interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
lemma equiv_rewrite : βF1,F2,F3. F1 β‘ F2 β F1 β‘ F3 β F2 β‘ F3. intros; intro; rewrite < H; rewrite < H1; reflexivity. qed.
lemma equiv_sym : βa,b.a β‘ b β b β‘ a. intros 4;symmetry;apply H;qed.
interpretation "S" 'my_S x = (S x).
interpretation "O" 'my_O = O.
-notation "x + y" non associative with precedence 50 for @{'my_plus $x $y}.
-notation "x * y" non associative with precedence 55 for @{'my_mult $x $y}.
+notation "x + y" non associative with precedence 55 for @{'my_plus $x $y}.
+notation "x * y" non associative with precedence 60 for @{'my_mult $x $y}.
notation "x = y" non associative with precedence 45 for @{'my_eq $x $y}.
notation > "'S' x" non associative with precedence 40 for @{'my_S $x}.
notation < "'S' βx" non associative with precedence 40 for @{'my_S $x}.
interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
definition equiv β Ξ»F1,F2. βv.[[ F1 ]]v = [[ F2 ]]v.
notation "hvbox(a \nbsp break mstyle color #0000ff (β‘) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }.
-notation > "a β‘ b" non associative with precedence 50 for @{ equiv $a $b }.
+notation > "a β‘ b" non associative with precedence 55 for @{ equiv $a $b }.
interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
lemma min_1_sem: βF,v.min 1 [[ F ]]v = [[ F ]]v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed.
lemma max_0_sem: βF,v.max [[ F ]]v 0 = [[ F ]]v. intros; cases (sem_bool F v); rewrite > H; reflexivity; qed.
interpretation "Substitution for Formula" 'substitution b a t = (subst b a t).
definition equiv β Ξ»F1,F2. βv.[[ F1 ]]v = [[ F2 ]]v.
notation "hvbox(a \nbsp break mstyle color #0000ff (β‘) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }.
-notation > "a β‘ b" non associative with precedence 50 for @{ equiv $a $b }.
+notation > "a β‘ b" non associative with precedence 55 for @{ equiv $a $b }.
interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
(* Test 2
(p
\atop
(ident i < n)) f"
-non associative with precedence 60 for
+non associative with precedence 65 for
@{ 'product $n (Ξ»${ident i}:$xx1.$p) (Ξ»${ident i}:$xx2.$f) }.
notation < "(mstyle scriptlevel 1 scriptsizemultiplier 1.7(Ξ ) Β
)
\below
((ident i < n)) f"
-non associative with precedence 60 for
+non associative with precedence 65 for
@{ 'product $n (Ξ»_:$xx1.$xx3) (Ξ»${ident i}:$xx2.$f) }.
interpretation "big product" 'product n p f = (pi_p n p f).
notation > "'Pi' (ident x) < n | p . term 46 f"
-non associative with precedence 60
+non associative with precedence 65
for @{ 'product $n (Ξ»${ident x}.$p) (Ξ»${ident x}.$f) }.
notation > "'Pi' (ident x) β€ n | p . term 46 f"
-non associative with precedence 60
+non associative with precedence 65
for @{ 'product (S $n) (Ξ»${ident x}.$p) (Ξ»${ident x}.$f) }.
notation > "'Pi' (ident x) < n . term 46 f"
-non associative with precedence 60
+non associative with precedence 65
for @{ 'product $n (Ξ»_.true) (Ξ»${ident x}.$f) }.
*)
| conv: βG.βA,B,C.βi. conv B C β
TJ G A B β TJ G B (Sort i) β TJ G A C.
-notation "hvbox(G break β’ A : B)" non associative with precedence 50 for @{'TJ $G $A $B}.
+notation "hvbox(G break β’ A : B)" non associative with precedence 55 for @{'TJ $G $A $B}.
interpretation "type judgement" 'TJ G A B = (TJ G A B).
(* ninverter TJ_inv2 for TJ (%?%) : Prop. *)
[ nil β 0
| cons a tl β S (length A tl)].
-notation "|M|" non associative with precedence 60 for @{'norm $M}.
+notation "|M|" non associative with precedence 65 for @{'norm $M}.
interpretation "norm" 'norm l = (length ? l).
nlet rec nth n (A:Type) (l:list A) (d:A) β
for @{ 'ndivides $a $b }.
notation "hvbox(a break + b)"
- left associative with precedence 50
+ left associative with precedence 55
for @{ 'plus $a $b }.
notation "hvbox(a break - b)"
- left associative with precedence 50
+ left associative with precedence 55
for @{ 'minus $a $b }.
notation "hvbox(a break * b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'times $a $b }.
notation "hvbox(a break \middot b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'middot $a $b }.
notation "hvbox(a break \mod b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'module $a $b }.
notation < "a \frac b"
for @{ 'divide $a $b }.
notation "a \over b"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'divide $a $b }.
notation "hvbox(a break / b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'divide $a $b }.
-notation "- term 60 a" with precedence 60
+notation "- term 65 a" with precedence 65
for @{ 'uminus $a }.
notation "a !"
for @{ 'fact $a }.
notation "\sqrt a"
- non associative with precedence 60
+ non associative with precedence 65
for @{ 'sqrt $a }.
notation "hvbox(a break \lor b)"
notation "hvbox(a break β b)" non associative with precedence 45
for @{ 'subseteq $a $b }. (* \subseteq *)
-notation "hvbox(a break β© b)" left associative with precedence 55
+notation "hvbox(a break β© b)" left associative with precedence 60
for @{ 'intersects $a $b }. (* \cap *)
-notation "hvbox(a break βͺ b)" left associative with precedence 50
+notation "hvbox(a break βͺ b)" left associative with precedence 55
for @{ 'union $a $b }. (* \cup *)
notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
for @{ 'apart $a $b}.
notation "hvbox(a break \circ b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'compose $a $b }.
-notation < "β \ensp a" with precedence 55 for @{ 'downarrow $a }.
-notation > "β a" with precedence 55 for @{ 'downarrow $a }.
+notation < "β \ensp a" with precedence 60 for @{ 'downarrow $a }.
+notation > "β a" with precedence 60 for @{ 'downarrow $a }.
-notation "hvbox(U break β V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
+notation "hvbox(U break β V)" non associative with precedence 60 for @{ 'fintersects $U $V }.
-notation "βa" with precedence 55 for @{ 'uparrow $a }.
+notation "βa" with precedence 60 for @{ 'uparrow $a }.
-notation "hvbox(a break β b)" with precedence 55 for @{ 'funion $a $b }.
+notation "hvbox(a break β b)" with precedence 60 for @{ 'funion $a $b }.
notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
notation > "x β© y" with precedence 45 for @{'Vdash2 $x $y ?}.
notation > "x β©β½ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
notation "x (β© \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
-notation > "β© " with precedence 60 for @{'Vdash ?}.
-notation "(β© \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
+notation > "β© " with precedence 65 for @{'Vdash ?}.
+notation "(β© \sub term 90 c) " with precedence 65 for @{'Vdash $c}.
notation < "maction (mstyle color #ff0000 (Ββ¦Β)) (t)"
non associative with precedence 90 for @{'hide $t}.
#A; #B; #H; napply (fi β¦ H); nassumption.
nqed.
-notation ". r" with precedence 50 for @{'fi $r}.
+notation ". r" with precedence 55 for @{'fi $r}.
interpretation "fi" 'fi r = (fi' ?? r).
ndefinition and_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
- x1...xn are bound in E and P, H is bound in P
- H is an identifier that will have the type of E in P
- P is the proof that the two existentially quantified predicates are equal*)
-notation > "β list1 ident x sep , . term 56 E / ident nE ; term 19 H" with precedence 20
+notation > "β list1 ident x sep , . term 61 E / ident nE ; term 19 H" with precedence 20
for @{ 'Sig_gen
${ fold right @{ 'End } rec acc @{ ('Next (Ξ»${ident x}.${ident x}) $acc) } }
${ fold right @{ $E } rec acc @{ Ξ»${ident x}.$acc } }
((Ex S (Ξ»w.ee x w β§ True) β¨ True)) =_1 ((Ex S (Ξ»w.ee y w β§ True) β¨ True)).
#S m x y E; napply (.=_1 (βw. E / E ; ((E βͺ_1 #) βͺ_1 #)) βͺ_1 #). //; nqed.
*)
-
\ No newline at end of file
+
interpretation "o-algebra overlap" 'overlap a b = (fun11 ?? (fun11 ?? (oa_overlap ?) a) b).
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (β§) \below (\emsp) \nbsp term 90 p)"
-non associative with precedence 50 for @{ 'oa_meet $p }.
+non associative with precedence 55 for @{ 'oa_meet $p }.
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (β§) \below (ident i β βI) break term 90 p)"
-non associative with precedence 50 for @{ 'oa_meet_mk (Ξ»${ident i}:$I.$p) }.
+non associative with precedence 55 for @{ 'oa_meet_mk (Ξ»${ident i}:$I.$p) }.
-(*notation > "hovbox(β§ f)" non associative with precedence 60
+(*notation > "hovbox(β§ f)" non associative with precedence 65
for @{ 'oa_meet $f }.
interpretation "o-algebra meet" 'oa_meet f =
(fun12 ?? (oa_meet ??) f).
(fun12 ?? (oa_meet ??) (mk_unary_morphism ?? f ?)).
*)
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (β¨) \below (\emsp) \nbsp term 90 p)"
-non associative with precedence 50 for @{ 'oa_join $p }.
+non associative with precedence 55 for @{ 'oa_join $p }.
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (β¨) \below (ident i β βI) break term 90 p)"
-non associative with precedence 50 for @{ 'oa_join_mk (Ξ»${ident i}:$I.$p) }.
+non associative with precedence 55 for @{ 'oa_join_mk (Ξ»${ident i}:$I.$p) }.
(*CSC
-notation > "hovbox(β¨ f)" non associative with precedence 60
+notation > "hovbox(β¨ f)" non associative with precedence 65
for @{ 'oa_join $f }.
interpretation "o-algebra join" 'oa_join f =
(fun12 ?? (oa_join ??) f).
notation < "hovbox(a β¨ b)" left associative with precedence 49
for @{ 'oa_join_mk (Ξ»${ident i}:$_.match $i with [ true β $a | false β $b ]) }.
-notation > "hovbox(β¨ f)" non associative with precedence 59
+notation > "hovbox(β¨ f)" non associative with precedence 64
for @{ 'oa_join $f }.
notation > "hovbox(a β¨ b)" left associative with precedence 49
for @{ 'oa_join (mk_unary_morphism BOOL ? (Ξ»x__:bool.match x__ with [ true β $a | false β $b ]) (IF_THEN_ELSE_p ? $a $b)) }.
interpretation "star" 'pk a = (k ? a).
interpretation "or" 'plus a b = (o ? a b).
-notation "a Β· b" non associative with precedence 60 for @{ 'pc $a $b}.
+notation "a Β· b" non associative with precedence 65 for @{ 'pc $a $b}.
interpretation "cat" 'pc a b = (c ? a b).
(* to get rid of \middot *)
nqed.
ndefinition lo β Ξ»S:Alpha.Ξ»a,b:pre S.β©\fst a + \fst b,\snd a || \snd bβͺ.
-notation "a β b" left associative with precedence 60 for @{'oplus $a $b}.
+notation "a β b" left associative with precedence 65 for @{'oplus $a $b}.
interpretation "oplus" 'oplus a b = (lo ? a b).
ndefinition lc β Ξ»S:Alpha.Ξ»bcast:βS:Alpha.βE:pitem S.pre S.Ξ»a,b:pre S.
[ false β β©e1 Β· \fst b, \snd bβͺ
| true β β©e1 Β· \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))βͺ]].
-notation < "a β b" left associative with precedence 60 for @{'lc $op $a $b}.
+notation < "a β b" left associative with precedence 65 for @{'lc $op $a $b}.
interpretation "lc" 'lc op a b = (lc ? op a b).
-notation > "a β b" left associative with precedence 60 for @{'lc eclose $a $b}.
+notation > "a β b" left associative with precedence 65 for @{'lc eclose $a $b}.
ndefinition lk β Ξ»S:Alpha.Ξ»bcast:βS:Alpha.βE:pitem S.pre S.Ξ»a:pre S.
match a with [ mk_pair e1 b1 β
interpretation "lk" 'lk op a = (lk ? op a).
notation > "a ^ β" non associative with precedence 75 for @{'lk eclose $a}.
-notation > "β’" non associative with precedence 60 for @{eclose ?}.
+notation > "β’" non associative with precedence 65 for @{eclose ?}.
nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S β
match E with
[ pz β β© 0, false βͺ
| po E1 E2 β β’E1 β β’E2
| pc E1 E2 β β’E1 β β© E2, false βͺ
| pk E β β©(\fst (β’E))^*,trueβͺ].
-notation < "β’ x" non associative with precedence 60 for @{'eclose $x}.
+notation < "β’ x" non associative with precedence 65 for @{'eclose $x}.
interpretation "eclose" 'eclose x = (eclose ? x).
-notation > "β’ x" non associative with precedence 60 for @{'eclose $x}.
+notation > "β’ x" non associative with precedence 65 for @{'eclose $x}.
ndefinition reclose β Ξ»S:Alpha.Ξ»p:pre S.let p' β β’\fst p in β©\fst p',\snd p || \snd p'βͺ.
interpretation "reclose" 'eclose x = (reclose ? x).
STOP
notation > "\move term 90 x term 90 E"
-non associative with precedence 60 for @{move ? $x $E}.
+non associative with precedence 65 for @{move ? $x $E}.
nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S β
match E with
[ pz β β© β
, false βͺ
| po e1 e2 β \move x e1 β \move x e2
| pc e1 e2 β \move x e1 β \move x e2
| pk e β (\move x e)^β ].
-notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}.
-notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}.
+notation < "\move\shy x\shy E" non associative with precedence 65 for @{'move $x $E}.
+notation > "\move term 90 x term 90 E" non associative with precedence 65 for @{'move $x $E}.
interpretation "move" 'move x E = (move ? x E).
ndefinition rmove β Ξ»S:Alpha.Ξ»x:S.Ξ»e:pre S. \move x (\fst e).
nqed.
-notation > "x β¦* E" non associative with precedence 60 for @{move_star ? $x $E}.
+notation > "x β¦* E" non associative with precedence 65 for @{move_star ? $x $E}.
nlet rec move_star (S : decidable) w E on w : bool Γ (pre S) β
match w with
[ nil β E
interpretation "star" 'pk a = (k ? a).
interpretation "or" 'plus a b = (o ? a b).
-notation "a Β· b" non associative with precedence 60 for @{ 'pc $a $b}.
+notation "a Β· b" non associative with precedence 65 for @{ 'pc $a $b}.
interpretation "cat" 'pc a b = (c ? a b).
(* to get rid of \middot *)
nqed.
ndefinition lo β Ξ»S:Alpha.Ξ»a,b:pre S.β©\fst a + \fst b,\snd a || \snd bβͺ.
-notation "a β b" left associative with precedence 60 for @{'oplus $a $b}.
+notation "a β b" left associative with precedence 65 for @{'oplus $a $b}.
interpretation "oplus" 'oplus a b = (lo ? a b).
ndefinition lc β Ξ»S:Alpha.Ξ»bcast:βS:Alpha.βE:pitem S.pre S.Ξ»a,b:pre S.
[ false β β©e1 Β· \fst b, \snd bβͺ
| true β β©e1 Β· \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))βͺ]].
-notation < "a β b" left associative with precedence 60 for @{'lc $op $a $b}.
+notation < "a β b" left associative with precedence 65 for @{'lc $op $a $b}.
interpretation "lc" 'lc op a b = (lc ? op a b).
-notation > "a β b" left associative with precedence 60 for @{'lc eclose $a $b}.
+notation > "a β b" left associative with precedence 65 for @{'lc eclose $a $b}.
ndefinition lk β Ξ»S:Alpha.Ξ»bcast:βS:Alpha.βE:pitem S.pre S.Ξ»a:pre S.
match a with [ mk_pair e1 b1 β
interpretation "lk" 'lk op a = (lk ? op a).
notation > "a^β" non associative with precedence 90 for @{'lk eclose $a}.
-notation > "β’" non associative with precedence 60 for @{eclose ?}.
+notation > "β’" non associative with precedence 65 for @{eclose ?}.
nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S β
match E with
[ pz β β© β
, false βͺ
| po E1 E2 β β’E1 β β’E2
| pc E1 E2 β β’E1 β β© E2, false βͺ
| pk E β β©(\fst (β’E))^*,trueβͺ].
-notation < "β’ x" non associative with precedence 60 for @{'eclose $x}.
+notation < "β’ x" non associative with precedence 65 for @{'eclose $x}.
interpretation "eclose" 'eclose x = (eclose ? x).
-notation > "β’ x" non associative with precedence 60 for @{'eclose $x}.
+notation > "β’ x" non associative with precedence 65 for @{'eclose $x}.
ndefinition reclose β Ξ»S:Alpha.Ξ»p:pre S.let p' β β’\fst p in β©\fst p',\snd p || \snd p'βͺ.
interpretation "reclose" 'eclose x = (reclose ? x).
STOP
notation > "\move term 90 x term 90 E"
-non associative with precedence 60 for @{move ? $x $E}.
+non associative with precedence 65 for @{move ? $x $E}.
nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S β
match E with
[ pz β β© β
, false βͺ
| po e1 e2 β \move x e1 β \move x e2
| pc e1 e2 β \move x e1 β \move x e2
| pk e β (\move x e)^β ].
-notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}.
-notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}.
+notation < "\move\shy x\shy E" non associative with precedence 65 for @{'move $x $E}.
+notation > "\move term 90 x term 90 E" non associative with precedence 65 for @{'move $x $E}.
interpretation "move" 'move x E = (move ? x E).
ndefinition rmove β Ξ»S:Alpha.Ξ»x:S.Ξ»e:pre S. \move x (\fst e).
nqed.
-notation > "x β¦* E" non associative with precedence 60 for @{move_star ? $x $E}.
+notation > "x β¦* E" non associative with precedence 65 for @{move_star ? $x $E}.
nlet rec move_star (S : decidable) w E on w : bool Γ (pre S) β
match w with
[ nil β E
}.
*)
-notation "hvbox(A break β B)" right associative with precedence 50 for @{ 'arrows $A $B }.
+notation "hvbox(A break β B)" right associative with precedence 55 for @{ 'arrows $A $B }.
interpretation "arrows1" 'arrows A B = (unary_morphism1 A B).
interpretation "arrows" 'arrows A B = (unary_morphism A B).
for @{ eq_rel ? (eq0 ?) $a $b }.
interpretation "setoid symmetry" 'invert r = (sym ???? r).
-notation ".= r" with precedence 50 for @{'trans $r}.
+notation ".= r" with precedence 55 for @{'trans $r}.
interpretation "trans" 'trans r = (trans ????? r).
-notation > ".=_0 r" with precedence 50 for @{'trans_x0 $r}.
+notation > ".=_0 r" with precedence 55 for @{'trans_x0 $r}.
interpretation "trans_x0" 'trans_x0 r = (trans ????? r).
nrecord unary_morphism (A,B: setoid) : Type[0] β {
interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r).
interpretation "setoid symmetry" 'invert r = (sym ???? r).
-notation ".=_1 r" with precedence 50 for @{'trans_x1 $r}.
+notation ".=_1 r" with precedence 55 for @{'trans_x1 $r}.
interpretation "trans1" 'trans r = (trans1 ????? r).
interpretation "trans" 'trans r = (trans ????? r).
interpretation "trans1_x1" 'trans_x1 r = (trans1 ????? r).
interpretation "setoid2 symmetry" 'invert r = (sym2 ???? r).
interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r).
interpretation "setoid symmetry" 'invert r = (sym ???? r).
-notation ".= r" with precedence 50 for @{'trans $r}.
+notation ".= r" with precedence 55 for @{'trans $r}.
interpretation "trans2" 'trans r = (trans2 ????? r).
interpretation "trans1" 'trans r = (trans1 ????? r).
interpretation "trans" 'trans r = (trans ????? r).
id_neutral_right: βo1,o2. βa: arrows o1 o2. comp ??? a (id o2) = a
}.
-notation "hvbox(A break β B)" right associative with precedence 50 for @{ 'arrows $A $B }.
+notation "hvbox(A break β B)" right associative with precedence 55 for @{ 'arrows $A $B }.
interpretation "arrows" 'arrows A B = (unary_morphism A B).
notation > "ππ term 90 A" non associative with precedence 90 for @{ 'id $A }.
| oL : βa:A.βi.βf:π a i β Ord A. Ord A.
notation "0" non associative with precedence 90 for @{ 'oO }.
-notation "Ξ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
-notation "x+1" non associative with precedence 50 for @{'oS $x }.
+notation "Ξ term 90 f" non associative with precedence 55 for @{ 'oL $f }.
+notation "x+1" non associative with precedence 55 for @{'oS $x }.
interpretation "ordinals Zero" 'oO = (oO ?).
interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
(*
-notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
-notation > "U β½ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
+notation < "term 90 U \sub (term 90 x)" non associative with precedence 55 for @{ 'famU $U $x }.
+notation > "U β½ term 90 x" non associative with precedence 55 for @{ 'famU $U $x }.
interpretation "famU" 'famU U x = (famU ? U x).
ndefinition coverage : βA:Ax.βU:Ξ©^A.Ξ©^A β Ξ»A,U.{ a | a β U }.
-notation "βU" non associative with precedence 55 for @{ 'coverage $U }.
+notation "βU" non associative with precedence 60 for @{ 'coverage $U }.
interpretation "coverage cover" 'coverage U = (coverage ? U).
D*)
-notation "βF" non associative with precedence 55
+notation "βF" non associative with precedence 60
for @{ 'fished $F }.
ndefinition fished : βA:Ax.βF:Ξ©^A.Ξ©^A β Ξ»A,F.{ a | a β F }.
| oL : βa:A.βi.βf:π a i β Ord A. Ord A.
notation "0" non associative with precedence 90 for @{ 'oO }.
-notation "x+1" non associative with precedence 50 for @{'oS $x }.
-notation "Ξ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
+notation "x+1" non associative with precedence 55 for @{'oS $x }.
+notation "Ξ term 90 f" non associative with precedence 55 for @{ 'oL $f }.
interpretation "ordinals Zero" 'oO = (oO ?).
interpretation "ordinals Succ" 'oS x = (oS ? x).
| oS y β let U_n β famU A U y in U_n βͺ { x | βi.ππ¦[π x i] β U_n}
| oL a i f β { x | βj.x β famU A U (f j) } ].
-notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
-notation > "U β½ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
+notation < "term 90 U \sub (term 90 x)" non associative with precedence 55 for @{ 'famU $U $x }.
+notation > "U β½ term 90 x" non associative with precedence 55 for @{ 'famU $U $x }.
interpretation "famU" 'famU U x = (famU ? U x).
for @{ 'ndivides $a $b }.
notation "hvbox(a break + b)"
- left associative with precedence 50
+ left associative with precedence 55
for @{ 'plus $a $b }.
notation "hvbox(a break - b)"
- left associative with precedence 50
+ left associative with precedence 55
for @{ 'minus $a $b }.
notation "hvbox(a break * b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'times $a $b }.
notation "hvbox(a break \middot b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'middot $a $b }.
notation "hvbox(a break \mod b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'module $a $b }.
notation < "a \frac b"
for @{ 'divide $a $b }.
notation "a \over b"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'divide $a $b }.
notation "hvbox(a break / b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'divide $a $b }.
-notation "- term 60 a" with precedence 60
+notation "- term 65 a" with precedence 65
for @{ 'uminus $a }.
notation "a !"
for @{ 'fact $a }.
notation "\sqrt a"
- non associative with precedence 60
+ non associative with precedence 65
for @{ 'sqrt $a }.
notation "hvbox(a break \lor b)"
notation "hvbox(a break β b)" non associative with precedence 45
for @{ 'subseteq $a $b }. (* \subseteq *)
-notation "hvbox(a break β© b)" left associative with precedence 55
+notation "hvbox(a break β© b)" left associative with precedence 60
for @{ 'intersects $a $b }. (* \cap *)
-notation "hvbox(a break βͺ b)" left associative with precedence 50
+notation "hvbox(a break βͺ b)" left associative with precedence 55
for @{ 'union $a $b }. (* \cup *)
notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
for @{ 'apart $a $b}.
notation "hvbox(a break \circ b)"
- left associative with precedence 55
+ left associative with precedence 60
for @{ 'compose $a $b }.
-notation < "β \ensp a" with precedence 55 for @{ 'downarrow $a }.
-notation > "β a" with precedence 55 for @{ 'downarrow $a }.
+notation < "β \ensp a" with precedence 60 for @{ 'downarrow $a }.
+notation > "β a" with precedence 60 for @{ 'downarrow $a }.
-notation "hvbox(U break β V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
+notation "hvbox(U break β V)" non associative with precedence 60 for @{ 'fintersects $U $V }.
-notation "βa" with precedence 55 for @{ 'uparrow $a }.
+notation "βa" with precedence 60 for @{ 'uparrow $a }.
-notation "hvbox(a break β b)" with precedence 55 for @{ 'funion $a $b }.
+notation "hvbox(a break β b)" with precedence 60 for @{ 'funion $a $b }.
notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
notation > "x β© y" with precedence 45 for @{'Vdash2 $x $y ?}.
notation > "x β©β½ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
notation "x (β© \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
-notation > "β© " with precedence 60 for @{'Vdash ?}.
-notation "(β© \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
+notation > "β© " with precedence 65 for @{'Vdash ?}.
+notation "(β© \sub term 90 c) " with precedence 65 for @{'Vdash $c}.
notation < "maction (mstyle color #ff0000 (Ββ¦Β)) (t)"
non associative with precedence 90 for @{'hide $t}.
[ nil β O
| cons a tl β S (length A tl)].
-notation "|M|" non associative with precedence 60 for @{'norm $M}.
+notation "|M|" non associative with precedence 65 for @{'norm $M}.
interpretation "norm" 'norm l = (length ? l).
lemma length_append: βA.βl1,l2:list A.
(* concatenation *)
definition cat : βS,l1,l2,w.Prop β
Ξ»S.Ξ»l1,l2.Ξ»w:word S.βw1,w2.w1 @ w2 = w β§ l1 w1 β§ l2 w2.
-notation "a Β· b" non associative with precedence 60 for @{ 'middot $a $b}.
+notation "a Β· b" non associative with precedence 65 for @{ 'middot $a $b}.
interpretation "cat lang" 'middot a b = (cat ? a b).
let rec flatten (S : DeqSet) (l : list (word S)) on l : word S β
]
qed.
-notation > "x β¦* E" non associative with precedence 60 for @{moves ? $x $E}.
+notation > "x β¦* E" non associative with precedence 65 for @{moves ? $x $E}.
let rec moves (S : DeqSet) w e on w : pre S β
match w with
[ nil β e
qed.
definition lo β Ξ»S:DeqSet.Ξ»a,b:pre S.β©\fst a + \fst b,\snd a β¨ \snd bβͺ.
-notation "a β b" left associative with precedence 60 for @{'oplus $a $b}.
+notation "a β b" left associative with precedence 65 for @{'oplus $a $b}.
interpretation "oplus" 'oplus a b = (lo ? a b).
lemma lo_def: βS.βi1,i2:pitem S.βb1,b2. β©i1,b1βͺββ©i2,b2βͺ=β©i1+i2,b1β¨b2βͺ.
definition pre_concat_r β Ξ»S:DeqSet.Ξ»i:pitem S.Ξ»e:pre S.
match e with [ mk_Prod i1 b β β©i Β· i1, bβͺ].
-notation "i β e" left associative with precedence 60 for @{'lhd $i $e}.
+notation "i β e" left associative with precedence 65 for @{'lhd $i $e}.
interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
lemma eq_to_ex_eq: βS.βA,B:word S β Prop.
]
].
-notation "a βΉ b" left associative with precedence 60 for @{'tril eclose $a $b}.
+notation "a βΉ b" left associative with precedence 65 for @{'tril eclose $a $b}.
interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
-notation "β’" non associative with precedence 60 for @{eclose ?}.
+notation "β’" non associative with precedence 65 for @{eclose ?}.
let rec eclose (S: DeqSet) (i: pitem S) on i : pre S β
match i with
| pc i1 i2 β β’i1 βΉ i2
| pk i β β©(\fst (β’i))^*,trueβͺ].
-notation "β’ x" non associative with precedence 60 for @{'eclose $x}.
+notation "β’ x" non associative with precedence 65 for @{'eclose $x}.
interpretation "eclose" 'eclose x = (eclose ? x).
lemma eclose_plus: βS:DeqSet.βi1,i2:pitem S.
(**************************************************************************)
notation < "mstyle mathsize big color #ff0000 background #0000ff scriptsizemultiplier 0.8 (x)"
- non associative with precedence 50 for @{'red $x}.
+ non associative with precedence 55 for @{'red $x}.
definition red : βX:Type.βt:X.X β Ξ»T.Ξ»t.t.
interpretation "red" 'red x = (red _ x).
projects / helm.git / commitdiff