class "orange" {
[ { @@("html/specification#v2" "Version 2") * }
{ "\"basic_2\"" * }
- { [ "\"A2\"" @("http://matita.cs.unibo.it/" "Matita 0.99.3")
- "October 2015" "" "" ""
+ { [ "\"B\"" @("http://matita.cs.unibo.it/" "Matita 0.99.3")
+ "October 2015" "November 2018" "" ""
"" *
]
- [ "\"A1\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2")
+ [ "\"A\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2")
"April 2011" "June 2014" "October 2014" "August 2015"
@@("html/documentation#ldV2a" "V2a") + " " + @@("html/documentation#ldR2c" "R2c") *
]
}
]
[ "Abandoned" ""
- "" @("http://coq.inria.fr/" "Coq 7.3.1")
- "March 2008" "" "" "February 2011"
- "" *
+ [ "" @("http://coq.inria.fr/" "Coq 7.3.1")
+ "March 2008" "" "" "February 2011"
+ "" *
+ ]
]
}
class "red"
[ @@("html/specification#v1" "Version 1") "\"basic_1\""
- "" @("http://coq.inria.fr/" "Coq 7.3.1")
- "May 2004" "December 2005" "November 2006" "May 2008"
- @@("html/documentation#ldV1a" "V1a") + " " + @@("html/documentation#ldJ1a" "J1a") *
+ [ "\"A\"" @("http://coq.inria.fr/" "Coq 7.3.1")
+ "May 2004" "December 2005" "November 2006" "May 2008"
+ @@("html/documentation#ldV1a" "V1a") + " " + @@("html/documentation#ldJ1a" "J1a") *
+ ]
]
}
+++ /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/rt_conversion/lpce.ma".
-include "basic_2/dynamic/cnv.ma".
-
-(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-
-theorem cnv_cpce_trans_lpce (h) (G):
- ∀L1,T1,T2. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T2 → ⦃G,L1⦄ ⊢ T1 !*[h] →
- ∀L2. ⦃G,L1⦄ ⊢ ⬌η[h] L2 → ⦃G,L2⦄ ⊢ T2 !*[h].
-#h #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
-[ #G #L1 #s #_ #L2 #_ //
-| #G #K1 #V1 #_ #Y2 #HY
- elim (lpce_inv_pair_sn … HY) -HY #K2 #V2 #HK #HV #H destruct
\ No newline at end of file
--- /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/rt_conversion/cpce.ma".
+include "basic_2/dynamic/cnv_preserve.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+theorem cnv_cpce_mono (a) (h) (G) (L) (T):
+ ∀T1. ⦃G,L⦄ ⊢ T ⬌η[h] T1 → ⦃G,L⦄ ⊢ T ![a,h] →
+ ∀T2. ⦃G,L⦄ ⊢ T ⬌η[h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h] T2.
+#h #G #L #T @(fqup_wf_ind (Ⓣ) … G L T) -G -L -T
+#G0 #L0 #T0 #IH #T1
+@(insert_eq_0 … G0) #G
+@(insert_eq_0 … L0) #L
+@(insert_eq_0 … T0) #T
+* -G -L -T
+[ #G #L1 #s #_ #_ #_ #_ #L2 #_ //
--- /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 "static_2/s_computation/fqup_weight.ma".
+include "basic_2/rt_conversion/lpce.ma".
+include "basic_2/dynamic/cnv_drops.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+theorem cnv_cpce_trans_lpce (h) (G):
+ ∀L1,T1,T2. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T2 → ⦃G,L1⦄ ⊢ T1 !*[h] →
+ ∀L2. ⦃G,L1⦄ ⊢ ⬌η[h] L2 → ⦃G,L2⦄ ⊢ T2 !*[h].
+#h #G #L1 #T1 @(fqup_wf_ind (Ⓣ) … G L1 T1) -G -L1 -T1
+#G0 #L0 #T0 #IH #T2
+@(insert_eq_0 … G0) #G
+@(insert_eq_0 … L0) #L1
+@(insert_eq_0 … T0) #T1
+* -G -L1 -T1
+[ #G #L1 #s #_ #_ #_ #_ #L2 #_ //
+| #G #K1 #V1 #HT #HL #HG #H0 #Y2 #HY2 destruct
+ elim (cnv_inv_zero … H0) -H0 #Z #Y #X #HV1 #H destruct
+ elim (lpce_inv_pair_sn … HY2) -HY2 #K2 #V2 #HK12 #HV12 #H destruct
+ /4 width=6 by cnv_zero, fqu_fqup, fqu_lref_O/
+| #n #G #K1 #V1 #s #_ #HT #HL #HG #H0 #Y2 #HY2 destruct
+ elim (cnv_inv_zero … H0) -H0 #Z #Y #X #HV1 #H destruct
+ elim (lpce_inv_pair_sn … HY2) -HY2 #K2 #V2 #HK12 #HV12 #H destruct
+ /4 width=6 by cnv_zero, fqu_fqup, fqu_lref_O/
+| #n #p #G #K1 #V1 #W1 #W2 #T1 #HVT1 #HW12 #HT #HL #HG #H0 #Y2 #HY2 destruct
+ elim (cnv_inv_zero … H0) -H0 #Z #Y #X #HV1 #H destruct
+ elim (lpce_inv_pair_sn … HY2) -HY2 #K2 #V2 #HK12 #HV12 #H destruct
+| #I #G #K1 #T1 #U1 #i #H0 #HTU1 #HT #HL #HG #H0 #Y2 #HY2 destruct
+ elim (cnv_inv_lref … H0) -H0 #Z1 #Y1 #Hi #H destruct
+ elim (lpce_inv_bind_sn … HY2) -HY2 #Z2 #K2 #HK12 #_ #H destruct
+ @(cnv_lifts … K2 … (Ⓣ) … HTU1) [| /3 width=1 by drops_refl, drops_drop/ ] -U1
+ /3 width=6 by fqu_fqup/
+| #p #I #G #K1 #V1 #V2 #T1 #T2 #HV12 #HT12 #HT #HL #HG #H0 #K2 #HK12 destruct
+ elim (cnv_inv_bind … H0) -H0 #HV1 #HT1
+ /4 width=8 by lpce_pair, cnv_bind/
+| * #G #L1 #V1 #V2 #T1 #T2 #HV12 #HT12 #HT #HL #HG #H0 #L2 #HK12 destruct
+
\ No newline at end of file
--- /dev/null
+include "basic_2/rt_transition/lpr.ma".
+include "basic_2/rt_conversion/lpce.ma".
+include "basic_2/dynamic/cnv_preserve.ma".
+
+lemma cpce_cpm_conf_lpce_lpr (a) (h) (n) (G):
+ ∀L1,T1. ⦃G,L1⦄ ⊢ T1 ![a,h] →
+ ∀U1. ⦃G,L1⦄ ⊢ T1 ⬌η[h] U1 → ∀K1. ⦃G,L1⦄ ⊢ ⬌η[h] K1 →
+ ∀T2. ⦃G,L1⦄ ⊢ T1 ➡[n,h] T2 → ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 →
+ ∃∃K2,U2. ⦃G,K1⦄ ⊢ ➡[h] K2 & ⦃G,L2⦄ ⊢ ⬌η[h] K2 & ⦃G,K2⦄ ⊢ U1 ➡[n,h] U2 & ⦃G,L2⦄ ⊢ T2 ⬌η[h] U2.
+#a #h #n #G #L1 #T1 #HT1
+letin o ≝ (sd_O h)
+lapply (cnv_fwd_fsb … o … HT1) -HT1 #H
+@(fsb_ind_fpbg … H) -G -L1 -T1 #G #L1 #T1 #_ #IH
+#U1
+
+#H elim H -G -L1 -T1 -U1
+[ #G #L1 elim L1 -L1 [| #L1 #I1 #IH ] #s #K1 #HLK1 #X2 #HX2 #Y2 #HY2
+ elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn destruct
+ [ lapply (lpr_inv_atom_sn … HY2) -HY2 #H destruct
+ lapply (lpce_inv_atom_sn … HLK1) -HLK1 #H destruct
+ /3 width=6 by cpce_sort, cpm_sort, ex4_2_intro/
+ | elim (lpr_inv_bind_sn … HY2) -HY2 #I2 #L2 #HL12 #HI12 #H destruct
+ elim (lpce_inv_bind_sn … HLK1) -HLK1 #J1 #K0 #HLK1 #HIJ1 #H destruct
+ elim (IH s ? HLK1 (⋆((next h)^n s)) … HL12) -IH -HLK1 -HL12
+ [| /2 width=1 by cpm_sort/ ] #K2 #U2 #HK12 #HLK2 #H1s #H2s
+
+| #G #L1 #s elim L1 -L1
+ [ #Y2 #HY2 #X2 #HX2 #K1 #HLK1
+ lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
+ /3 width=6 by cpce_sort, ex4_2_intro/
+ | #L1 #I1 #IH #Y2 #HY2 #X2 #HX2 #K1 #HLK1
+ lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
+
+
+| #n #G #K1 #V1 #V2 #X1 #HV12 #_ #HX1 #X2 #HX2 #Y2 #HY2
+ elim (lpr_inv_pair_sn … HY2) -HY2 #K2 #W1 #HK12 #HVW1 #H destruct
+ lapply (cpce_inv_ldef_sn … HX2) -HX2 #H destruct
+ elim (lifts_total W1 (𝐔❴1❵)) #X2 #HX2
+ @(ex2_intro … X2) [ @(cpm_delta … HX2) /3 width=5 by _/
+
+ /3 width=3 by cpce_ldef, ex2_intro/
+ |
\ No newline at end of file
(* *)
(**************************************************************************)
-include "ground_2/xoa/ex_2_4.ma".
include "basic_2/notation/relations/pconveta_5.ma".
include "basic_2/rt_computation/cpms.ma".
| cpce_ldef: ∀G,K,V. cpce h G (K.ⓓV) (#0) (#0)
| cpce_ldec: ∀n,G,K,V,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s →
cpce h G (K.ⓛV) (#0) (#0)
-| cpce_eta : ∀n,p,G,K,V,W,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W.T →
- cpce h G (K.ⓛV) (#0) (+ⓛW.ⓐ#0.#1)
+| cpce_eta : ∀n,p,G,K,V,W1,W2,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W1.T →
+ cpce h G K W1 W2 → cpce h G (K.ⓛV) (#0) (+ⓛW2.ⓐ#0.#1)
| cpce_lref: ∀I,G,K,T,U,i. cpce h G K (#i) T →
⬆*[1] T ≘ U → cpce h G (K.ⓘ{I}) (#↑i) U
| cpce_bind: ∀p,I,G,K,V1,V2,T1,T2.
.
interpretation
- "context-sensitive parallel eta-conversion (term)"
- 'PConvEta h G L T1 T2 = (cpce h G L T1 T2).
+ "context-sensitive parallel eta-conversion (term)"
+ 'PConvEta h G L T1 T2 = (cpce h G L T1 T2).
(* Basic inversion lemmas ***************************************************)
[ #G #L #s #_ //
| #G #K #V #_ //
| #n #G #K #V #s #_ #_ //
-| #n #p #G #K #V #W #T #_ #H destruct
+| #n #p #G #K #V #W1 #W2 #T #_ #_ #H destruct
| #I #G #K #T #U #i #_ #_ #H destruct
| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct
| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
[ #G #L #s #_ #_ //
| #G #K #V #_ #_ //
| #n #G #K #V #s #_ #_ #_ //
-| #n #p #G #K #V #W #T #_ #_ #H destruct
+| #n #p #G #K #V #W1 #W2 #T #_ #_ #_ #H destruct
| #I #G #K #T #U #i #_ #_ #H #_ destruct
| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
lemma cpce_inv_ldec_sn (h) (G) (K) (X2):
∀V. ⦃G,K.ⓛV⦄ ⊢ #0 ⬌η[h] X2 →
∨∨ ∃∃n,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s & #0 = X2
- | ∃∃n,p,W,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W.T & +ⓛW.ⓐ#0.#1 = X2.
+ | ∃∃n,p,W1,W2,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W1.T & ⦃G,K⦄ ⊢ W1 ⬌η[h] W2 & +ⓛW2.ⓐ#0.#1 = X2.
#h #G #Y #X2 #X
@(insert_eq_0 … (Y.ⓛX)) #Y1
@(insert_eq_0 … (#0)) #X1
[ #G #L #s #H #_ destruct
| #G #K #V #_ #H destruct
| #n #G #K #V #s #HV #_ #H destruct /3 width=3 by ex2_2_intro, or_introl/
-| #n #p #G #K #V #W #T #HV #_ #H destruct /3 width=6 by or_intror, ex2_4_intro/
+| #n #p #G #K #V #W1 #W2 #T #HV #HW #_ #H destruct /3 width=8 by ex3_5_intro, or_intror/
| #I #G #K #T #U #i #_ #_ #H #_ destruct
| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
[ #G #L #s #H #_ destruct
| #G #K #V #H #_ destruct
| #n #G #K #V #s #_ #H #_ destruct
-| #n #p #G #K #V #W #T #_ #H #_ destruct
+| #n #p #G #K #V #W1 #W2 #T #_ #_ #H #_ destruct
| #I #G #K #T #U #i #Hi #HTU #H1 #H2 destruct /2 width=3 by ex2_intro/
| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
[ #G #L #s #H destruct
| #G #K #V #H destruct
| #n #G #K #V #s #_ #H destruct
-| #n #p #G #K #V #W #T #_ #H destruct
+| #n #p #G #K #V #W1 #W2 #T #_ #_ #H destruct
| #I #G #K #T #U #i #_ #_ #H destruct
| #p #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/
| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
[ #G #L #s #H destruct
| #G #K #V #H destruct
| #n #G #K #V #s #_ #H destruct
-| #n #p #G #K #V #W #T #_ #H destruct
+| #n #p #G #K #V #W1 #W2 #T #_ #_ #H destruct
| #I #G #K #T #U #i #_ #_ #H destruct
| #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
| #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/
--- /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 "static_2/syntax/cext2.ma".
+include "basic_2/rt_conversion/cpce.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR BINDERS ********************)
+
+definition cpce_ext (h) (G): relation3 lenv bind bind ≝ cext2 (cpce h G).
+
+interpretation
+ "context-sensitive parallel eta-conversion (binder)"
+ 'PConvEta h G L I1 I2 = (cpce_ext h G L I1 I2).
include "static_2/relocation/lex.ma".
include "basic_2/notation/relations/pconveta_4.ma".
-include "basic_2/rt_conversion/cpce.ma".
+include "basic_2/rt_conversion/cpce_ext.ma".
(* PARALLEL ETA-CONVERSION FOR FULL LOCAL ENVIRONMENTS **********************)
"parallel eta-conversion on all entries (local environment)"
'PConvEta h G L1 L2 = (lpce h G L1 L2).
+(* Basic properties *********************************************************)
+
+lemma lpce_bind (h) (G):
+ ∀K1,K2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 →
+ ∀I1,I2. ⦃G,K1⦄ ⊢ I1 ⬌η[h] I2 → ⦃G,K1.ⓘ{I1}⦄ ⊢ ⬌η[h] K2.ⓘ{I2}.
+/2 width=1 by lex_bind/ qed.
+
(* Advanced properties ******************************************************)
lemma lpce_pair (h) (G):
∀L2. ⦃G,⋆⦄ ⊢ ⬌η[h] L2 → L2 = ⋆.
/2 width=2 by lex_inv_atom_sn/ qed-.
+lemma lpce_inv_bind_sn (h) (G):
+ ∀I1,L2,K1. ⦃G,K1.ⓘ{I1}⦄ ⊢ ⬌η[h] L2 →
+ ∃∃I2,K2. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & ⦃G,K1⦄ ⊢ I1 ⬌η[h] I2 & L2 = K2.ⓘ{I2}.
+/2 width=1 by lex_inv_bind_sn/ qed-.
+
lemma lpce_inv_atom_dx (h) (G):
∀L1. ⦃G,L1⦄ ⊢ ⬌η[h] ⋆ → L1 = ⋆.
/2 width=2 by lex_inv_atom_dx/ qed-.
+lemma lpce_inv_bind_dx (h) (G):
+ ∀I2,L1,K2. ⦃G,L1⦄ ⊢ ⬌η[h] K2.ⓘ{I2} →
+ ∃∃I1,K1. ⦃G,K1⦄ ⊢ ⬌η[h] K2 & ⦃G,K1⦄ ⊢ I1 ⬌η[h] I2 & L1 = K1.ⓘ{I1}.
+/2 width=1 by lex_inv_bind_dx/ qed-.
+
(* Advanced inversion lemmas ************************************************)
lemma lpce_inv_unit_sn (h) (G):
<table name="basic_2_sum"/>
<subsection name="B">Stage "B"</subsection>
-<!--
- <news class="alpha" date="Ongoing.">
- Context-sensitive subject equivalence
- for native type assignment.
- </news>
--->
- <news class="alpha" date="2018 November 1.">
+ <news class="beta" date="2018 November 1.">
Extended (λδ-2) and restricted (λδ-1) type rules justified.
</news>
<news class="alpha" date="2018 September 21.">
[ { "rt-conversion" * } {
[ { "context-sensitive parallel eta-conversion" * } {
[ [ "for lenvs on all entries" ] "lpce ( ⦃?,?⦄ ⊢ ⬌η[?] ? )" * ]
+ [ [ "for binders" ] "cpce_ext" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ]
[ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ]
}
]
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* This file was generated by xoa.native: do not edit *********************)
-
-(* multiple existental quantifier (2, 4) *)
-
-notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1)"
- non associative with precedence 20
- for @{ 'Ex4 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) }.
-
-notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1)"
- non associative with precedence 20
- for @{ 'Ex4 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) }.
-
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* This file was generated by xoa.native: do not edit *********************)
-
-include "basics/pts.ma".
-
-include "ground_2/notation/xoa/ex_2_4.ma".
-
-(* multiple existental quantifier (2, 4) *)
-
-inductive ex2_4 (A0,A1,A2,A3:Type[0]) (P0,P1:A0→A1→A2→A3→Prop) : Prop ≝
- | ex2_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → ex2_4 ? ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (2, 4)" 'Ex4 P0 P1 = (ex2_4 ? ? ? ? P0 P1).
-
<key name="objects">ground_2/xoa</key>
<key name="notations">ground_2/notation/xoa</key>
<key name="include">basics/pts.ma</key>
- <key name="ex">2 4</key>
<key name="ex">5 1</key>
<key name="ex">5 7</key>
<key name="ex">9 3</key>
projects / helm.git / commitdiff