--- /dev/null
+notation "hvbox( l1 ● break l2 )"
+ right associative with precedence 47
+ for @{ 'DoubleSemicolon $l1 $l2 }.
+
+notation "hvbox( hd ◗ break tl )"
+ right associative with precedence 47
+ for @{ 'Semicolon $hd $tl }.
+
+notation "hvbox( hd ◖ break tl )"
+ left associative with precedence 47
+ for @{ 'Comma $hd $tl }.
+
+lemma tmp1 (l1) (l2) (p): l1 ◗ l2 ◗ p = l1 ◗ (l2 ◗ p).
+// qed.
+
+lemma tmp2 (p) (l1) (l2): p ◖ l1 ◖ l2 = (p ◖ l1) ◖ l2.
+// qed.
+
+lemma tmp3 (p1) (p2) (p3): p1 ● p2 ● p3 = p1 ● (p2 ● p3).
+// qed.
+
+lemma tmp4 (l1) (p) (l2): l1 ◗ p ◖ l2 = l1 ◗ (p ◖ l2).
+// qed.
+
+lemma tmp5 (p1) (l) (p2): p1 ◖ l ● p2 = (p1 ◖ l) ● p2.
+// qed.
+
+lemma tmp6 (p1) (p2) (l): p1 ● p2 ◖ l = p1 ● (p2 ◖ l).
+// qed.
+
+lemma tmp7 (l) (p1) (p2): l ◗ p1 ● p2 = l ◗ (p1 ● p2).
+// qed.
+
+lemma tmp8 (p1) (l) (p2): p1 ● l ◗ p2 = p1 ● (l ◗ p2).
+// 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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( hd ◖ break tl )"
+ left associative with precedence 47
+ for @{ 'BlackHalfCircleLeft $hd $tl }.
--- /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 DELAYED UPDATING ********************************************)
+
+notation "hvbox( hd ◗ break tl )"
+ right associative with precedence 47
+ for @{ 'BlackHalfCircleRight $hd $tl }.
+++ /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 DELAYED UPDATING ********************************************)
-
-notation "hvbox( hd , break tl )"
- right associative with precedence 50
- for @{ 'Comma $hd $tl }.
+++ /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 DELAYED UPDATING ********************************************)
-
-notation "hvbox( hd ; break tl )"
- right associative with precedence 47
- for @{ 'Semicolon $hd $tl }.
--- /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 DELAYED UPDATING ********************************************)
+
+notation "hvbox( ↑ [ term 46 t1 ] break term 75 t2 )"
+ non associative with precedence 75
+ for @{ 'UpArrow $t1 $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 DELAYED UPDATING ********************************************)
+
+notation < "hvbox( ↑ ❨ term 46 k, break term 46 p, break term 46 f ❩ )"
+ non associative with precedence 75
+ for @{ 'UpArrow $S $k $p $f }.
+
+notation > "hvbox( ↑ ❨ term 46 k, break term 46 p, break term 46 f ❩ )"
+ non associative with precedence 75
+ for @{ 'UpArrow ? $k $p $f }.
+
+notation > "hvbox( ↑ { term 46 S } ❨ break term 46 k, break term 46 p, break term 46 f ❩ )"
+ non associative with precedence 75
+ for @{ 'UpArrow $S $k $p $f }.
--- /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 DELAYED UPDATING ********************************************)
+
+notation "hvbox( t1 ➡ 'd' 'f' [ break term 46 p, break term 46 q ] break term 46 t2 )"
+ non associative with precedence 45
+ for @{ 'BlackRightArrow $t1 $p $q $t2 }.
include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/syntax/path_balanced.ma".
include "delayed_updating/substitution/fsubst.ma".
-(*
-include "delayed_updating/notation/functions/pitchforkleftarrow_3.ma".
-*)
+include "delayed_updating/notation/relations/black_rightarrow_4.ma".
(* DELAYED FOCALIZED REDUCTION **********************************************)
inductive dfr (p) (q) (t): predicate preterm ≝
| dfr_beta (b) (n):
- let r ≝ p;;(𝗔;b;;(𝗟;q,𝗱❨n❩)) in
- r ϵ t → ⊓⊗b → dfr p q t (t[⋔r←t⋔p,𝗦])
+ let r ≝ p●𝗔◗b●𝗟◗q◖𝗱❨n❩ in
+ r ϵ t → ⊓⊗b → dfr p q t (t[⋔r←t⋔(p◖𝗦)])
.
-(*
+
interpretation
- "focalized substitution (preterm)"
- 'PitchforkLeftArrow t p u = (fsubst p u t).
-*)
+ "delayed focalized reduction (preterm)"
+ 'BlackRightArrow t1 p q t2 = (dfr p q t1 t2).
definition fsubst (p) (u): preterm → preterm ≝
λt,q.
- ∨∨ ∃∃r. r ϵ u & p ϵ ▵t & p;;r = q
- | ∧∧ q ϵ t & (∀r. p;;r = q → ⊥)
+ ∨∨ ∃∃r. r ϵ u & p ϵ ▵t & p●r = q
+ | ∧∧ q ϵ t & (∀r. p●r = q → ⊥)
.
interpretation
--- /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 "ground/relocation/tr_compose.ma".
+include "ground/relocation/tr_uni.ma".
+include "delayed_updating/syntax/path.ma".
+include "delayed_updating/notation/functions/uparrow_4.ma".
+include "delayed_updating/notation/functions/uparrow_2.ma".
+
+(* LIFT FOR PATH ***********************************************************)
+
+(* Note: inner numeric labels are not liftable, so they are removed *)
+rec definition lift_gen (A:Type[0]) (k:?→?→A) (p) (f) on p ≝
+match p with
+[ list_empty ⇒ k 𝐞 f
+| list_lcons l q ⇒
+ match l with
+ [ label_node_d n ⇒
+ match q with
+ [ list_empty ⇒ lift_gen (A) (λp. k (𝗱❨f@❨n❩❩◗p)) q f
+ | list_lcons _ _ ⇒ lift_gen (A) k q (f∘𝐮❨n❩)
+ ]
+ | label_edge_L ⇒ lift_gen (A) (λp. k (𝗟◗p)) q (⫯f)
+ | label_edge_A ⇒ lift_gen (A) (λp. k (𝗔◗p)) q f
+ | label_edge_S ⇒ lift_gen (A) (λp. k (𝗦◗p)) q f
+ ]
+].
+
+interpretation
+ "lift (gneric)"
+ 'UpArrow A k p f = (lift_gen A k p f).
+
+definition proj_path (p:path) (f:tr_map) ≝ p.
+
+definition proj_rmap (p:path) (f:tr_map) ≝ f.
+
+interpretation
+ "lift (path)"
+ 'UpArrow f p = (lift_gen ? proj_path p f).
+
+interpretation
+ "lift (relocation map)"
+ 'UpArrow p f = (lift_gen ? proj_rmap p f).
+
+(* Basic constructions ******************************************************)
+
+lemma lift_L (A) (k) (p) (f):
+ ↑❨(λp. k (𝗟◗p)), p, ⫯f❩ = ↑{A}❨k, 𝗟◗p, f❩.
+// qed.
+
+(* Basic constructions with proj_path ***************************************)
+
+lemma lift_append (p) (f) (q):
+ q●↑[f]p = ↑❨(λp. proj_path (q●p)), p, f❩.
+#p elim p -p
+[ //
+| #l #p #IH #f #q cases l
+ [
+ | <lift_L in ⊢ (???%);
+ >(list_append_rcons_sn ? q) in ⊢ (???(??(λ_.%)??));
+
+ <IH
+ normalize >IH
+ | //
+
+(* Constructions with append ************************************************)
+
+theorem lift_append_A (p2) (p1) (f):
+ (↑[f]p1)●𝗔◗↑[↑[p1]f]p2 = ↑[f](p1●𝗔◗p2).
+#p2 #p1 elim p1 -p1
+[ #f normalize
+++ /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 "ground/relocation/tr_pap.ma".
-include "delayed_updating/syntax/path.ma".
-
-(* DEPHI FOR PATH ***********************************************************)
-
-rec definition path_dephi (f) (p) on p ≝
-match p with
-[ list_empty ⇒ 𝐞
-| list_lcons l q ⇒
- match l with
- [ label_node_d n ⇒ 𝗱❨f@❨n❩❩;path_dephi f q
- | label_edge_L ⇒ 𝗟;path_dephi (𝟏⨮f) q
- | label_edge_A ⇒ 𝗔;path_dephi f q
- | label_edge_S ⇒ 𝗦;path_dephi f q
- ]
-].
lemma bdd_inv_in_comp_gen:
∀t,p. t ϵ 𝐃𝛗 → p ϵ t →
- ∨∨ ∃∃n. #n ⇔ t & 𝗱❨n❩;𝐞 = p
- | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t & 𝗱❨n❩;q = p
- | ∃∃u,q. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t & 𝗟;q = p
- | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t & 𝗔;q = p
- | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t & 𝗦;q = p
+ ∨∨ ∃∃n. #n ⇔ t & 𝗱❨n❩◗𝐞 = p
+ | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t & 𝗱❨n❩◗q = p
+ | ∃∃u,q. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t & 𝗟◗q = p
+ | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t & 𝗔◗q = p
+ | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t & 𝗦◗q = p
.
#t #p #H elim H -H
[ #n * /3 width=3 by or5_intro0, ex2_intro/
qed-.
lemma bdd_inv_in_comp_d:
- ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ t →
+ ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩◗q ϵ t →
∨∨ ∧∧ #n ⇔ t & 𝐞 = q
| ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t
.
qed-.
lemma bdd_inv_in_root_d:
- ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ ▵t →
+ ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩◗q ϵ ▵t →
∨∨ ∧∧ #n ⇔ t & 𝐞 = q
| ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛗n.u ⇔ t
.
qed-.
lemma bdd_inv_in_comp_L:
- ∀t,q. t ϵ 𝐃𝛗 → 𝗟;q ϵ t →
+ ∀t,q. t ϵ 𝐃𝛗 → 𝗟◗q ϵ t →
∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t
.
#t #q #Ht #Hq
qed-.
lemma bdd_inv_in_root_L:
- ∀t,q. t ϵ 𝐃𝛗 → 𝗟;q ϵ ▵t →
+ ∀t,q. t ϵ 𝐃𝛗 → 𝗟◗q ϵ ▵t →
∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛌.u ⇔ t.
#t #q #Ht * #r #Hq
elim (bdd_inv_in_comp_L … Ht Hq) -Ht -Hq
qed-.
lemma bdd_inv_in_comp_A:
- ∀t,q. t ϵ 𝐃𝛗 → 𝗔;q ϵ t →
+ ∀t,q. t ϵ 𝐃𝛗 → 𝗔◗q ϵ t →
∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t
.
#t #q #Ht #Hq
qed-.
lemma bdd_inv_in_root_A:
- ∀t,q. t ϵ 𝐃𝛗 → 𝗔;q ϵ ▵t →
+ ∀t,q. t ϵ 𝐃𝛗 → 𝗔◗q ϵ ▵t →
∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ ▵u & @v.u ⇔ t
.
#t #q #Ht * #r #Hq
qed-.
lemma bdd_inv_in_comp_S:
- ∀t,q. t ϵ 𝐃𝛗 → 𝗦;q ϵ t →
+ ∀t,q. t ϵ 𝐃𝛗 → 𝗦◗q ϵ t →
∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t
.
#t #q #Ht #Hq
qed-.
lemma bdd_inv_in_root_S:
- ∀t,q. t ϵ 𝐃𝛗 → 𝗦;q ϵ ▵t →
+ ∀t,q. t ϵ 𝐃𝛗 → 𝗦◗q ϵ ▵t →
∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ ▵v & @v.u ⇔ t
.
#t #q #Ht * #r #Hq
(* Advanced inversions ******************************************************)
lemma bbd_mono_in_root_d:
- ∀l,n,p,t. t ϵ 𝐃𝛗 → p,𝗱❨n❩ ϵ ▵t → p,l ϵ ▵t → 𝗱❨n❩ = l.
+ ∀l,n,p,t. t ϵ 𝐃𝛗 → p◖𝗱❨n❩ ϵ ▵t → p◖l ϵ ▵t → 𝗱❨n❩ = l.
#l #n #p elim p -p
[ #t #Ht <list_cons_comm <list_cons_comm #Hn #Hl
elim (bdd_inv_in_root_d … Ht Hn) -Ht -Hn *
include "ground/lib/list_rcons.ma".
include "ground/notation/functions/element_e_0.ma".
-include "ground/notation/functions/double_semicolon_2.ma".
+include "ground/notation/functions/black_circle_2.ma".
include "delayed_updating/syntax/label.ma".
-include "delayed_updating/notation/functions/semicolon_2.ma".
-include "delayed_updating/notation/functions/comma_2.ma".
+include "delayed_updating/notation/functions/black_halfcircleright_2.ma".
+include "delayed_updating/notation/functions/black_halfcircleleft_2.ma".
(* PATH *********************************************************************)
interpretation
"left cons (paths)"
- 'Semicolon l p = (list_lcons label l p).
+ 'BlackHalfCircleRight l p = (list_lcons label l p).
interpretation
"append (paths)"
- 'DoubleSemicolon l1 l2 = (list_append label l1 l2).
+ 'BlackCircle l1 l2 = (list_append label l1 l2).
interpretation
"right cons (paths)"
- 'Comma p l = (list_append label p (list_lcons label l (list_empty label))).
+ 'BlackHalfCircleLeft p l = (list_append label p (list_lcons label l (list_empty label))).
(* This condition applies to a structural path *)
inductive pbc: predicate path ≝
-| pbc_empty: pbc 𝐞
-| pbc_redex: ∀b. pbc b → pbc (𝗔;b,𝗟)
-| pbc_after: ∀b1,b2. pbc b1 → pbc b2 → pbc (b1;;b2)
+| pbc_empty: pbc 𝐞
+| pbc_redex: ∀b. pbc b → pbc (𝗔◗b◖𝗟)
+| pbc_after: ∀b1,b2. pbc b1 → pbc b2 → pbc (b1●b2)
.
interpretation
| list_lcons l q ⇒
match l with
[ label_node_d n ⇒ path_structure q
- | label_edge_L ⇒ 𝗟;path_structure q
- | label_edge_A ⇒ 𝗔;path_structure q
- | label_edge_S ⇒ 𝗦;path_structure q
+ | label_edge_L ⇒ 𝗟◗path_structure q
+ | label_edge_A ⇒ 𝗔◗path_structure q
+ | label_edge_S ⇒ 𝗦◗path_structure q
]
].
definition preterm: Type[0] ≝ 𝒫❨path❩.
definition preterm_grafted: path → preterm → preterm ≝
- λp,t,q. p;;q ϵ t.
+ λp,t,q. p●q ϵ t.
interpretation
"grafted (preterm)"
'Pitchfork t p = (preterm_grafted p t).
definition preterm_root: preterm → preterm ≝
- λt,q. ∃r. q;;r ϵ t.
+ λt,q. ∃r. q●r ϵ t.
interpretation
"root (preterm)"
(* CONSTRUCTORS FOR PRETERM *************************************************)
definition preterm_node_0 (l): preterm ≝
- λp. l;𝐞 = p.
+ λp. l◗𝐞 = p.
definition preterm_node_1 (l): preterm → preterm ≝
- λt,p. ∃∃q. q ϵ t & l;q = p.
+ λt,p. ∃∃q. q ϵ t & l◗q = p.
definition preterm_node_2 (l1) (l2): preterm → preterm → preterm ≝
λt1,t2,p.
- ∨∨ ∃∃q. q ϵ t1 & l1;q = p
- | ∃∃q. q ϵ t2 & l2;q = p.
+ ∨∨ ∃∃q. q ϵ t1 & l1◗q = p
+ | ∃∃q. q ϵ t2 & l2◗q = p.
interpretation
"outer variable reference by depth (preterm)"
(* Basic Inversions *********************************************************)
lemma preterm_in_root_inv_lcons_oref:
- ∀p,l,n. l;p ϵ ▵#n →
+ ∀p,l,n. l◗p ϵ ▵#n →
∧∧ 𝗱❨n❩ = l & 𝐞 = p.
#p #l #n * #q
<list_append_lcons_sn #H0 destruct -H0
qed-.
lemma preterm_in_root_inv_lcons_iref:
- ∀t,p,l,n. l;p ϵ ▵𝛗n.t →
+ ∀t,p,l,n. l◗p ϵ ▵𝛗n.t →
∧∧ 𝗱❨n❩ = l & p ϵ ▵t.
#t #p #l #n * #q
<list_append_lcons_sn * #r #Hr #H0 destruct
qed-.
lemma preterm_in_root_inv_lcons_abst:
- ∀t,p,l. l;p ϵ ▵𝛌.t →
+ ∀t,p,l. l◗p ϵ ▵𝛌.t →
∧∧ 𝗟 = l & p ϵ ▵t.
#t #p #l * #q
<list_append_lcons_sn * #r #Hr #H0 destruct
qed-.
lemma preterm_in_root_inv_lcons_appl:
- ∀u,t,p,l. l;p ϵ ▵@u.t →
+ ∀u,t,p,l. l◗p ϵ ▵@u.t →
∨∨ ∧∧ 𝗦 = l & p ϵ ▵u
| ∧∧ 𝗔 = l & p ϵ ▵t.
#u #t #p #l * #q
["M"; "ℳ"; "𝕄"; "𝐌"; "Ⓜ"; ] ;
["n"; "𝕟"; "𝐧"; "𝛈"; "ⓝ"; ] ;
["N"; "ℕ"; "№"; "𝐍"; "Ⓝ"; ] ;
- ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "⊚"; "ø"; "○"; "●"; "𝐨"; "𝛉"; "ⓞ"; ] ;
+ ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "⊚"; "ø"; "○"; "●"; "◖"; "◗"; "𝐨"; "𝛉"; "ⓞ"; ] ;
["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹"; "Ⓞ"; ] ;
["p"; "π"; "𝕡"; "𝐩"; "𝛑"; "ⓟ"; ] ;
["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; "𝒫"; ] ;
projects / helm.git / commitdiff