\ /
V_______________________________________________________________ *)
+include "lambda-delta/substitution/lift_fun.ma".
include "lambda-delta/substitution/lift_weight.ma".
include "lambda-delta/reduction/tpr_main.ma".
+include "lambda-delta/reduction/tpr_ps.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
(* Confluence lemmas ********************************************************)
-lemma tpr_conf_sort_sort: βk1. ββT0. βk1 β T0 & βk1 β T0.
+lemma tpr_conf_sort_sort: βk. ββX. βk β X & βk β X.
/2/ qed.
-lemma tpr_conf_lref_lref: βi1. ββT0. #i1 β T0 & #i1 β T0.
+lemma tpr_conf_lref_lref: βi. ββX. #i β X & #i β X.
/2/ qed.
lemma tpr_conf_bind_bind:
- βI1,V11,V12,T11,T12,V22,T22. (
- βT1. #T1 < #V11 + #T11 + 1 β
- βT3,T4. T1 β T3 β T1 β T4 β
- ββT0. T3 β T0 & T4 β T0
+ βI,V0,V1,T0,T1,V2,T2. (
+ βX0:term. #X0 < #V0 + #T0 + 1 β
+ βX1,X2. X0 β X1 β X0 β X2 β
+ ββX. X1 β X & X2 β X
+ ) β
+ V0 β V1 β V0 β V2 β T0 β T1 β T0 β T2 β
+ ββX. π{I} V1. T1 β X & π{I} V2. T2 β X.
+#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
+elim (IH β¦ HV01 β¦ HV02) -HV01 HV02 // #V #HV1 #HV2
+elim (IH β¦ HT01 β¦ HT02) -HT01 HT02 IH /3 width=5/
+qed.
+
+lemma tpr_conf_bind_delta:
+ βV0,V1,T0,T1,V2,T2,T. (
+ βX0:term. #X0 < #V0 + #T0 + 1 β
+ βX1,X2. X0 β X1 β X0 β X2 β
+ ββX. X1 β X & X2 β X
) β
- V11 β V12 β T11 β T12 β
- V11 β V22 β T11 β T22 β
- ββT0. π{I1} V12. T12 β T0 & π{I1} V22. T22 β T0.
-#I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
-elim (IH β¦ HV1 β¦ HV2) -HV1 HV2 // #V #HV1 #HV2
-elim (IH β¦ HT1 β¦ HT2) -HT1 HT2 IH /3 width=5/
+ V0 β V1 β V0 β V2 β
+ T0 β T1 β T0 β T2 β β. π{Abbr} V2 β’ T2 [O,1] β« T β
+ ββX. π{Abbr} V1. T1 β X & π{Abbr} V2. T β X.
+#V0 #V1 #T0 #T1 #V2 #T2 #T #IH #HV01 #HV02 #HT01 #HT02 #HT2
+elim (IH β¦ HV01 β¦ HV02) -HV01 HV02 // #V #HV1 #HV2
+elim (IH β¦ HT01 β¦ HT02) -HT01 HT02 IH // -V0 T0 #T0 #HT10 #HT20
+elim (tpr_ps_bind β¦ HV2 HT20 β¦ HT2) -HT20 HT2 /3 width=5/
qed.
lemma tpr_conf_bind_zeta:
- βV11,V12,T11,T12,T22,T20. (
- βT1. #T1 < #V11 + #T11 +1 β
- βT3,T4. T1 β T3 β T1 β T4 β
- ββT0. T3 β T0 & T4 β T0
+ βX2,V0,V1,T0,T1,T. (
+ βX0:term. #X0 < #V0 + #T0 +1 β
+ βX1,X2. X0 β X1 β X0 β X2 β
+ ββX. X1 β X & X2 β X
) β
- V11 β V12 β T22 β T20 β T11 β T12 β β[O, 1] T22 β‘ T11 β
- ββT0. π{Abbr} V12. T12 β T0 & T20 β T0.
-#V11 #V12 #T11 #T12 #T22 #T20 #IH #HV112 #HT202 #HT112 #HT
-elim (tpr_inv_lift β¦ HT112 β¦ HT) -HT112 #T #HT12 #HT22
-lapply (tw_lift β¦ HT) -HT #HT
-elim (IH β¦ HT202 β¦ HT22) -HT202 HT22 IH /3/
+ V0 β V1 β T0 β T1 β T β X2 β β[O, 1] T β‘ T0 β
+ ββX. π{Abbr} V1. T1 β X & X2 β X.
+#X2 #V0 #V1 #T0 #T1 #T #IH #HV01 #HT01 #HTX2 #HT0
+elim (tpr_inv_lift β¦ HT01 β¦ HT0) -HT01 #U #HUT1 #HTU
+lapply (tw_lift β¦ HT0) -HT0 #HT0
+elim (IH β¦ HTX2 β¦ HTU) -HTX2 HTU IH /3/
qed.
lemma tpr_conf_flat_flat:
- βI1,V11,V12,T11,T12,V22,T22. (
- βT1. #T1 < #V11 + #T11 + 1 β
- βT3,T4. T1 β T3 β T1 β T4 β
- ββT0. T3 β T0 & T4 β T0
+ βI,V0,V1,T0,T1,V2,T2. (
+ βX0:term. #X0 < #V0 + #T0 + 1 β
+ βX1,X2. X0 β X1 β X0 β X2 β
+ ββX. X1 β X & X2 β X
) β
- V11 β V12 β T11 β T12 β
- V11 β V22 β T11 β T22 β
- ββT0. π{I1} V12. T12 β T0 & π{I1} V22. T22 β T0.
-#I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
-elim (IH β¦ HV1 β¦ HV2) -HV1 HV2 // #V #HV1 #HV2
-elim (IH β¦ HT1 β¦ HT2) -HT1 HT2 /3 width=5/
+ V0 β V1 β V0 β V2 β T0 β T1 β T0 β T2 β
+ ββT0. π{I} V1. T1 β T0 & π{I} V2. T2 β T0.
+#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
+elim (IH β¦ HV01 β¦ HV02) -HV01 HV02 // #V #HV1 #HV2
+elim (IH β¦ HT01 β¦ HT02) -HT01 HT02 /3 width=5/
qed.
lemma tpr_conf_flat_beta:
- βV11,V12,T12,V22,W2,T21,T22. (
- βT1. #T1 < #V11 + (#W2 + #T21 + 1) + 1 β
- βT3,T4. T1 β T3 β T1 β T4 β
- ββT0. T3 β T0 & T4 β T0
+ βV0,V1,T1,V2,W0,U0,T2. (
+ βX0:term. #X0 < #V0 + (#W0 + #U0 + 1) + 1 β
+ βX1,X2. X0 β X1 β X0 β X2 β
+ ββX. X1 β X & X2 β X
) β
- V11 β V12 β V11 β V22 β
- T21 β T22 β π{Abst} W2. T21 β T12 β
- ββT0. π{Appl} V12. T12 β T0 & π{Abbr} V22. T22 β T0.
-#V11 #V12 #T12 #V22 #W2 #T21 #T22 #IH #HV1 #HV2 #HT1 #HT2
-elim (tpr_inv_abst1 β¦ HT2) -HT2 #W1 #T1 #HW21 #HT21 #H destruct -T12;
-elim (IH β¦ HV1 β¦ HV2) -HV1 HV2 // #V #HV12 #HV22
-elim (IH β¦ HT21 β¦ HT1) -HT21 HT1 IH /3 width=5/
+ V0 β V1 β V0 β V2 β
+ U0 β T2 β π{Abst} W0. U0 β T1 β
+ ββX. π{Appl} V1. T1 β X & π{Abbr} V2. T2 β X.
+#V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H
+elim (tpr_inv_abst1 β¦ H) -H #W1 #U1 #HW01 #HU01 #H destruct -T1;
+elim (IH β¦ HV01 β¦ HV02) -HV01 HV02 // #V #HV1 #HV2
+elim (IH β¦ HT02 β¦ HU01) -HT02 HU01 IH /3 width=5/
qed.
-(*
+
lemma tpr_conf_flat_theta:
- βV11,V12,T12,V2,V22,W21,W22,T21,T22. (
- βT1. #T1 < #V11 + (#W21 + #T21 + 1) + 1 β
- βT3,T4. T1 β T3 β T1 β T4 β
- ββT0. T3 β T0 & T4 βT0
+ βV0,V1,T1,V2,V,W0,W2,U0,U2. (
+ βX0:term. #X0 < #V0 + (#W0 + #U0 + 1) + 1 β
+ βX1,X2. X0 β X1 β X0 β X2 β
+ ββX. X1 β X & X2 β X
) β
- V11 β V12 β V11 β V22 β β[O,1] V22 β‘ V2 β
- W21 β W22 β T21 β T22 β π{Abbr} W21. T21 β T12 β
- ββT0. π{Appl} V12. T12 β T0 & π{Abbr} W22. π{Appl} V2. T22 βT0.
-*)
-
+ V0 β V1 β V0 β V2 β β[O,1] V2 β‘ V β
+ W0 β W2 β U0 β U2 β π{Abbr} W0. U0 β T1 β
+ ββX. π{Appl} V1. T1 β X & π{Abbr} W2. π{Appl} V. U2 β X.
+#V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H
+elim (IH β¦ HV01 β¦ HV02) -HV01 HV02 // #VV #HVV1 #HVV2
+elim (lift_total VV 0 1) #VVV #HVV
+lapply (tpr_lift β¦ HVV2 β¦ HV2 β¦ HVV) #HVVV
+elim (tpr_inv_abbr1 β¦ H) -H *
+(* case 1: bind *)
+[ -HV2 HVV2 #WW #UU #HWW0 #HUU0 #H destruct -T1;
+ elim (IH β¦ HW02 β¦ HWW0) -HW02 HWW0 // #W #HW2 #HWW
+ elim (IH β¦ HU02 β¦ HUU0) -HU02 HUU0 IH // #U #HU2 #HUU
+ @ex2_1_intro
+ [2: @tpr_theta [5: @HVV1 |6: @HVV |7:// by {}; (*@HWW*) |8: @HUU |1,2,3,4:skip ]
+ |3: @tpr_bind [ @HW2 | @tpr_flat [ @HVVV | @HU2 ] ]
+ | skip
(* Confluence ***************************************************************)
-(*
+
lemma tpr_conf_aux:
- βT. (
- βT1. #T1 < #T β βT3,T4. T1 β T3 β T1 β T4 β
- ββT0. T3 β T0 & T4 β T0
+ βY0:term. (
+ βX0:term. #X0 < #Y0 β βX1,X2. X0 β X1 β X0 β X2 β
+ ββX. X1 β X & X2 β X
) β
- βU1,T1,T2. U1 β T1 β U1 β T2 β U1 = T β
- ββT0. T1 β T0 & T2 β T0.
-#T #IH #U1 #T1 #T2 * -U1 T1
-[ #k1 #H1 #H2 destruct -T;
+ βX0,X1,X2. X0 β X1 β X0 β X2 β X0 = Y0 β
+ ββX. X1 β X & X2 β X.
+#Y0 #IH #X0 #X1 #X2 * -X0 X1
+[ #k1 #H1 #H2 destruct -Y0;
lapply (tpr_inv_sort1 β¦ H1) -H1
-(* case 1: sort, sort *)
- #H1 destruct -T2 //
-| #i1 #H1 #H2 destruct -T;
+(* case 1: sort, sort *)
+ #H1 destruct -X2 //
+| #i1 #H1 #H2 destruct -Y0;
lapply (tpr_inv_lref1 β¦ H1) -H1
-(* case 2: lref, lref *)
- #H1 destruct -T2 //
-| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 #H1 #H2 destruct -T;
- lapply (tpr_inv_bind1 β¦ H1) -H1
- [
-
-theorem tpr_conf: βT,T1,T2. T β T1 β T β T2 β
- ββT0. T1 β T0 & T2 β T0.
+(* case 2: lref, lref *)
+ #H1 destruct -X2 //
+| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
+ elim (tpr_inv_bind1 β¦ H1) -H1 *
+(* case 3: bind, bind *)
+ [ #V2 #T2 #HV02 #HT02 #H destruct -X2
+ @tpr_conf_bind_bind /2 width=7/ (**) (* /3 width=7/ is too slow *)
+(* case 4: bind, delta *)
+ | #V2 #T2 #T #HV02 #HT02 #HT2 #H1 #H2 destruct -X2 I
+ @tpr_conf_bind_delta /2 width=9/ (**) (* /3 width=9/ is too slow *)
+(* case 5: bind, zeta *)
+ | #T #HT0 #HTX2 #H destruct -I
+ @tpr_conf_bind_zeta /2 width=8/ (**) (* /3 width=8/ is too slow *)
+ ]
+| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
+ elim (tpr_inv_flat1 β¦ H1) -H1 *
+(* case 6: flat, flat *)
+ [ #V2 #T2 #HV02 #HT02 #H destruct -X2
+ @tpr_conf_flat_flat /2 width=7/ (**) (* /3 width=7/ is too slow *)
+(* case 7: flat, beta *)
+ | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct -T0 X2 I
+ @tpr_conf_flat_beta /2 width=8/ (**) (* /3 width=8/ is too slow *)
+(* case 8: flat, theta *)
+ | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I
+ //
+theorem tpr_conf: βT0,T1,T2. T0 β T1 β T0 β T2 β
+ ββT. T1 β T & T2 β T.
#T @(tw_wf_ind β¦ T) -T /3 width=6/
qed.
*)
W21 β W22 β T21 β T22 β π{Abbr} W21. T21 β T12 β
ββT0. π{Appl} V12. T12 β T0 & π{Abbr} W22. π{Appl} V2. T22 βT0.
+lemma tpr_conf_bind_delta:
+ βV0,V1,T0,T1,V2,T2,T. (
+ βX. #X < #V0 + #T0 + 1 β
+ βX1,X2. X0 β X1 β X0 β X2 β
+ ββX. X1 β X & X2βX
+ ) β
+ V0 β V1 β V0 β V2 β
+ T0 β T1 β T0 β T2 β β. π{Abbr} V2 β’ T2 [O,1] β« T β
+ ββX. π{Abbr} V1. T1 β X & π{Abbr} V2. T β X.
\ No newline at end of file
interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1).
+inductive ex3_1 (A0:Type[0]) (P0,P1,P2:A0βProp) : Prop β
+ | ex3_1_intro: βx0. P0 x0 β P1 x0 β P2 x0 β ex3_1 ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3_1 ? P0 P1 P2).
+
inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0βA1βProp) : Prop β
| ex3_2_intro: βx0,x1. P0 x0 x1 β P1 x0 x1 β P2 x0 x1 β ex3_2 ? ? ? ? ?
.
interpretation "multiple existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3).
+inductive ex5_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4:A0βA1βA2βProp) : Prop β
+ | ex5_3_intro: βx0,x1,x2. P0 x0 x1 x2 β P1 x0 x1 x2 β P2 x0 x1 x2 β P3 x0 x1 x2 β P4 x0 x1 x2 β ex5_3 ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (5, 3)" 'Ex P0 P1 P2 P3 P4 = (ex5_3 ? ? ? P0 P1 P2 P3 P4).
+
+inductive ex5_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4:A0βA1βA2βA3βProp) : Prop β
+ | ex5_4_intro: βx0,x1,x2,x3. P0 x0 x1 x2 x3 β P1 x0 x1 x2 x3 β P2 x0 x1 x2 x3 β P3 x0 x1 x2 x3 β P4 x0 x1 x2 x3 β ex5_4 ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4).
+
inductive ex6_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5:A0βA1βA2βA3βA4βA5βProp) : Prop β
| ex6_6_intro: βx0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 β P1 x0 x1 x2 x3 x4 x5 β P2 x0 x1 x2 x3 x4 x5 β P3 x0 x1 x2 x3 x4 x5 β P4 x0 x1 x2 x3 x4 x5 β P5 x0 x1 x2 x3 x4 x5 β ex6_6 ? ? ? ? ? ? ? ? ? ? ? ?
.
interpretation "multiple existental quantifier (6, 6)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5).
+inductive ex7_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0βA1βA2βA3βA4βA5βProp) : Prop β
+ | ex7_6_intro: βx0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 β P1 x0 x1 x2 x3 x4 x5 β P2 x0 x1 x2 x3 x4 x5 β P3 x0 x1 x2 x3 x4 x5 β P4 x0 x1 x2 x3 x4 x5 β P5 x0 x1 x2 x3 x4 x5 β P6 x0 x1 x2 x3 x4 x5 β ex7_6 ? ? ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (7, 6)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
+
inductive or3 (P0,P1,P2:Prop) : Prop β
| or3_intro0: P0 β or3 ? ? ?
| or3_intro1: P1 β or3 ? ? ?
interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2).
+inductive or4 (P0,P1,P2,P3:Prop) : Prop β
+ | or4_intro0: P0 β or4 ? ? ? ?
+ | or4_intro1: P1 β or4 ? ? ? ?
+ | or4_intro2: P2 β or4 ? ? ? ?
+ | or4_intro3: P3 β or4 ? ? ? ?
+.
+
+interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3).
+
non associative with precedence 20
for @{ 'Ex (Ξ»${ident x0},${ident x1}.$P0) (Ξ»${ident x0},${ident x1}.$P1) }.
+notation "hvbox(ββ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (Ξ»${ident x0}.$P0) (Ξ»${ident x0}.$P1) (Ξ»${ident x0}.$P2) }.
+
notation "hvbox(ββ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
non associative with precedence 20
for @{ 'Ex (Ξ»${ident x0},${ident x1}.$P0) (Ξ»${ident x0},${ident x1}.$P1) (Ξ»${ident x0},${ident x1}.$P2) }.
non associative with precedence 20
for @{ 'Ex (Ξ»${ident x0},${ident x1},${ident x2},${ident x3}.$P0) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3}.$P1) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3}.$P2) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3}.$P3) }.
+notation "hvbox(ββ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+ non associative with precedence 20
+ for @{ 'Ex (Ξ»${ident x0},${ident x1},${ident x2}.$P0) (Ξ»${ident x0},${ident x1},${ident x2}.$P1) (Ξ»${ident x0},${ident x1},${ident x2}.$P2) (Ξ»${ident x0},${ident x1},${ident x2}.$P3) (Ξ»${ident x0},${ident x1},${ident x2}.$P4) }.
+
+notation "hvbox(ββ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+ non associative with precedence 20
+ for @{ 'Ex (Ξ»${ident x0},${ident x1},${ident x2},${ident x3}.$P0) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3}.$P1) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3}.$P2) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3}.$P3) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3}.$P4) }.
+
notation "hvbox(ββ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)"
non associative with precedence 20
for @{ 'Ex (Ξ»${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P0) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P1) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P2) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P3) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P4) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P5) }.
-notation "hvbox(Ò\88¨Ò\88¨ term 19 P0 break | term 19 P1 break | term 19 P2)"
+notation "hvbox(Γ’\88\83Γ’\88\83 ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
non associative with precedence 20
+ for @{ 'Ex (Ξ»${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P0) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P1) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P2) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P3) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P4) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P5) (Ξ»${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P6) }.
+
+notation "hvbox(β¨β¨ term 29 P0 break | term 29 P1 break | term 29 P2)"
+ non associative with precedence 30
for @{ 'Or $P0 $P1 $P2 }.
+notation "hvbox(β¨β¨ term 29 P0 break | term 29 P1 break | term 29 P2 break | term 29 P3)"
+ non associative with precedence 30
+ for @{ 'Or $P0 $P1 $P2 $P3 }.
+
projects / helm.git / commitdiff