+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ [ break term 46 h ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'BTPRed $h $G1 $L1 $T1 $G2 $L2 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≻ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'BTPRedProper $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'BTPRedStar $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedSubTy $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≻ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedSubTyProper $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedSubTyStar $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/btpredproper_8.ma".
+include "basic_2/notation/relations/predsubtyproper_8.ma".
include "basic_2/s_transition/fqu.ma".
include "basic_2/static/lfdeq.ma".
include "basic_2/rt_transition/lfpr_lfpx.ma".
interpretation
"proper parallel rst-transition (closure)"
- 'BTPRedProper h o G1 L1 T1 G2 L2 T2 = (fpb h o G1 L1 T1 G2 L2 T2).
+ 'PRedSubTyProper h o G1 L1 T1 G2 L2 T2 = (fpb h o G1 L1 T1 G2 L2 T2).
(* Basic properties *********************************************************)
[ #G #L2 #U #H2 elim (lfdeq_fqu_trans … H2 … HT) -K2
/3 width=5 by fpb_fqu, ex3_2_intro/
| #U #HTU #HnTU elim (lfdeq_cpx_trans … HT … HTU) -HTU
- /5 width=10 by fpb_cpx, cpx_lfdeq_conf_sn, tdeq_trans, tdeq_lfdeq_conf_sn, ex3_2_intro/
+ /5 width=10 by fpb_cpx, cpx_lfdeq_conf_sn, tdeq_trans, tdeq_lfdeq_conf, ex3_2_intro/
| #L2 #HKL2 #HnKL2 elim (lfdeq_lfpx_trans … HKL2 … HT) -HKL2
- /6 width=5 by fpb_lfpx, lfdeq_canc_sn, ex3_2_intro/ (* 2 lleq_canc_sn *)
+ /6 width=5 by fpb_lfpx, (* 2x *) lfdeq_canc_sn, ex3_2_intro/
]
qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/btpred_7.ma".
+include "basic_2/notation/relations/predsubty_8.ma".
+include "basic_2/static/ffdeq.ma".
include "basic_2/s_transition/fquq.ma".
include "basic_2/rt_transition/lfpr_lfpx.ma".
(* PARALLEL RST-TRANSITION FOR CLOSURES *************************************)
(* Basic_2A1: includes: fpbq_lleq *)
-inductive fpbq (h) (G1) (L1) (T1): relation3 genv lenv term ≝
-| fpbq_fquq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → fpbq h G1 L1 T1 G2 L2 T2
-| fpbq_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ⬈[h] T2 → fpbq h G1 L1 T1 G1 L1 T2
-| fpbq_lfpx: ∀L2. ⦃G1, L1⦄ ⊢ ⬈[h, T1] L2 → fpbq h G1 L1 T1 G1 L2 T1
+inductive fpbq (h) (o) (G1) (L1) (T1): relation3 genv lenv term ≝
+| fpbq_fquq : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → fpbq h o G1 L1 T1 G2 L2 T2
+| fpbq_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ⬈[h] T2 → fpbq h o G1 L1 T1 G1 L1 T2
+| fpbq_lfpx : ∀L2. ⦃G1, L1⦄ ⊢ ⬈[h, T1] L2 → fpbq h o G1 L1 T1 G1 L2 T1
+| ffpq_lfdeq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → fpbq h o G1 L1 T1 G2 L2 T2
.
interpretation
"parallel rst-transition (closure)"
- 'BTPRed h G1 L1 T1 G2 L2 T2 = (fpbq h G1 L1 T1 G2 L2 T2).
+ 'PRedSubTy h o G1 L1 T1 G2 L2 T2 = (fpbq h o G1 L1 T1 G2 L2 T2).
(* Basic properties *********************************************************)
-lemma fpbq_refl: ∀h. tri_reflexive … (fpbq h).
+lemma fpbq_refl: ∀h,o. tri_reflexive … (fpbq h o).
/2 width=1 by fpbq_cpx/ qed.
(* Basic_2A1: includes: cpr_fpbq *)
-lemma cpm_fpbq: ∀n,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → ⦃G, L, T1⦄ ≽[h] ⦃G, L, T2⦄.
+lemma cpm_fpbq: ∀n,h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → ⦃G, L, T1⦄ ≽[h, o] ⦃G, L, T2⦄.
/3 width=2 by fpbq_cpx, cpm_fwd_cpx/ qed.
-lemma lfpr_fpbq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → ⦃G, L1, T⦄ ≽[h] ⦃G, L2, T⦄.
+lemma lfpr_fpbq: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → ⦃G, L1, T⦄ ≽[h, o] ⦃G, L2, T⦄.
/3 width=1 by fpbq_lfpx, lfpr_fwd_lfpx/ qed.
(* Basic_2A1: removed theorems 2:
(**************************************************************************)
include "basic_2/static/aaa_fqus.ma".
+include "basic_2/static/aaa_ffdeq.ma".
include "basic_2/rt_transition/lfpx_aaa.ma".
include "basic_2/rt_transition/fpbq.ma".
(* Properties with atomic arity assignment for terms ************************)
-lemma fpbq_aaa_conf: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h] ⦃G2, L2, T2⦄ →
+lemma fpbq_aaa_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G2, L2, T2⦄ →
∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2.
-#h #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-/3 width=6 by lfpx_aaa_conf, cpx_aaa_conf, aaa_fquq_conf, ex_intro/
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
+/3 width=8 by lfpx_aaa_conf, cpx_aaa_conf, aaa_ffdeq_conf, aaa_fquq_conf, ex_intro/
qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/static/ffdeq.ma".
+include "basic_2/static/aaa_lfdeq.ma".
+
+(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
+
+(* Properties with degree-based equivalence on referred entries *************)
+
+lemma aaa_ffdeq_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ →
+ ∀A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → ⦃G2, L2⦄ ⊢ T2 ⁝ A.
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
+/2 width=7 by aaa_tdeq_conf_lfdeq/ qed-.
(* Properties with degree-based equivalence on referred entries *************)
-lemma aaa_tdeq_conf_fldeq: ∀h,o,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀T2. T1 ≛[h, o] T2 →
+lemma aaa_tdeq_conf_lfdeq: ∀h,o,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀T2. T1 ≛[h, o] T2 →
∀L2. L1 ≛[h, o, T1] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
#h #o #G #L1 #T1 #A #H elim H -G -L1 -T1 -A
[ #G #L1 #s1 #X #H1 elim (tdeq_inv_sort1 … H1) -H1 //
(* DEGREE-BASED EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES ****************)
-inductive ffdeq (h) (o) (G) (L1) (T): relation3 genv lenv term ≝
-| ffdeq_intro: ∀L2. L1 ≛[h, o, T] L2 → ffdeq h o G L1 T G L2 T
+inductive ffdeq (h) (o) (G) (L1) (T1): relation3 genv lenv term ≝
+| ffdeq_intro_sn: ∀L2,T2. L1 ≛[h, o, T1] L2 → T1 ≛[h, o] T2 →
+ ffdeq h o G L1 T1 G L2 T2
.
interpretation
"degree-based equivalence on referred entries (closure)"
'StarEqSn h o G1 L1 T1 G2 L2 T2 = (ffdeq h o G1 L1 T1 G2 L2 T2).
+(* Basic_properties *********************************************************)
+
+lemma ffdeq_intro_dx (h) (o) (G): ∀L1,L2,T2. L1 ≛[h, o, T2] L2 →
+ ∀T1. T1 ≛[h, o] T2 → ⦃G, L1, T1⦄ ≛[h, o] ⦃G, L2, T2⦄.
+/3 width=3 by ffdeq_intro_sn, tdeq_lfdeq_div/ qed.
+
(* Basic inversion lemmas ***************************************************)
-lemma ffdeq_inv_gen: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ →
- ∧∧ G1 = G2 & L1 ≛[h, o, T1] L2 & T1 = T2.
+lemma ffdeq_inv_gen_sn: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & L1 ≛[h, o, T1] L2 & T1 ≛[h, o] T2.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/
qed-.
+lemma ffdeq_inv_gen_dx: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & L1 ≛[h, o, T2] L2 & T1 ≛[h, o] T2.
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
+/3 width=3 by tdeq_lfdeq_conf, and3_intro/
+qed-.
+
(* Basic_2A1: removed theorems 6:
fleq_refl fleq_sym fleq_inv_gen
fleq_trans fleq_canc_sn fleq_canc_dx
(* Advanced properties ******************************************************)
lemma ffdeq_sym: ∀h,o. tri_symmetric … (ffdeq h o).
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -L1 -T1 /3 width=1 by ffdeq_intro, lfdeq_sym/
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -L1 -T1
+/3 width=1 by ffdeq_intro_dx, lfdeq_sym, tdeq_sym/
qed-.
(* Main properties **********************************************************)
theorem ffdeq_trans: ∀h,o. tri_transitive … (ffdeq h o).
#h #o #G1 #G #L1 #L #T1 #T * -G -L -T
-#L #HL1 #G2 #L2 #T2 * -G2 -L2 -T2 /3 width=3 by ffdeq_intro, lfdeq_trans/
+#L #T #HL1 #HT1 #G2 #L2 #T2 * -G2 -L2 -T2
+/4 width=5 by ffdeq_intro_sn, lfdeq_trans, tdeq_lfdeq_div, tdeq_trans/
qed-.
theorem ffdeq_canc_sn: ∀h,o,G,G1,G2,L,L1,L2,T,T1,T2.
(* Advanced properties ******************************************************)
lemma ffdeq_refl: ∀h,o. tri_reflexive … (ffdeq h o).
-/2 width=1 by ffdeq_intro/ qed.
+/2 width=1 by ffdeq_intro_sn/ qed.
∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
/2 width=7 by frees_tdeq_conf_lfdeq, tdeq_refl/ qed-.
-lemma tdeq_lfdeq_conf_sn: ∀h,o. s_r_confluent1 … (cdeq h o) (lfdeq h o).
+lemma tdeq_lfdeq_conf: ∀h,o. s_r_confluent1 … (cdeq h o) (lfdeq h o).
#h #o #L1 #T1 #T2 #HT12 #L2 *
/3 width=5 by frees_tdeq_conf, ex2_intro/
qed-.
+lemma tdeq_lfdeq_div: ∀h,o,T1,T2. T1 ≛[h, o] T2 →
+ ∀L1,L2. L1 ≛[h, o, T2] L2 → L1 ≛[h, o, T1] L2.
+/3 width=3 by tdeq_lfdeq_conf, tdeq_sym/ qed-.
+
lemma lfdeq_atom: ∀h,o,I. ⋆ ≛[h, o, ⓪{I}] ⋆.
/2 width=1 by lfxs_atom/ qed.
#h #o #b #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
[ #I #G #L2 #V2 #L1 #H elim (lfdeq_inv_zero_pair_dx … H) -H
#K1 #V1 #HV1 #HV12 #H destruct
- /3 width=7 by tdeq_lfdeq_conf_sn, fqu_lref_O, ex3_2_intro/
+ /3 width=7 by tdeq_lfdeq_conf, fqu_lref_O, ex3_2_intro/
| * [ #p ] #I #G #L2 #V #T #L1 #H
[ elim (lfdeq_inv_bind … H)
| elim (lfdeq_inv_flat … H)
elim (lfdeq_fqu_trans … HU2 … HK0) -K #K1 #U1 #HU1 #HU12 #HK12
elim (tdeq_fqu_trans … HU1 … HU0) -U #K3 #U3 #HU03 #HU31 #HK31
@(ex3_2_intro … K3 U3) (**) (* full auto too slow *)
- /3 width=5 by lfdeq_trans, tdeq_lfdeq_conf_sn, fqup_strap1, tdeq_trans/
+ /3 width=5 by lfdeq_trans, tdeq_lfdeq_conf, fqup_strap1, tdeq_trans/
]
qed-.
]
*)
[ { "uncounted context-sensitive parallel rt-computation" * } {
- [ [ "refinement for lenvs" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
+ [ [ "refinement for lenvs on selected entries" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
[ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_cpx" + "lfsx_cpxs" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
[ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
[ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
class "cyan"
[ { "rt-transition" * } {
[ { "uncounted parallel rst-transition" * } {
- [ [ "for closures" ] "fpbq" + "( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ]
- [ [ "proper for closures" ] "fpb" + "( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
+ [ [ "for closures" ] "fpbq" + "( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_aaa" * ]
+ [ [ "proper for closures" ] "fpb" + "( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
}
]
[ { "context-sensitive parallel r-transition" * } {
]
[ { "atomic arity assignment" * } {
[ [ "restricted refinement for lenvs" ] "lsuba" + "( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
- [ [ "for terms" ] "aaa" + "( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ]
+ [ [ "for terms" ] "aaa" + "( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_ffdeq" + "aaa_aaa" * ]
}
]
[ { "degree-based equivalence" * } {
}
]
[ { "syntactic equivalence" * } {
- [ [ "for lenvs on referred entries" ] "lfeq" + "( ? â\89¡[?] ? )" "lfeq_fqup" + "lfeq_fsle" * ]
+ [ [ "for lenvs on referred entries" ] "lfeq" + "( ? â\89\90[?] ? )" "lfeq_fqup" + "lfeq_fsle" * ]
}
]
[ { "generic extension of a context-sensitive relation" * } {
}
]
[ { "syntactic equivalence" * } {
- [ [ "for lenvs on selected entries" ] "lreq" + "( ? â\89¡[?] ? )" "lreq_length" + "lreq_lreq" * ]
+ [ [ "for lenvs on selected entries" ] "lreq" + "( ? â\89\90[?] ? )" "lreq_length" + "lreq_lreq" * ]
}
]
[ { "generic entrywise extension" * } {
projects / helm.git / commitdiff