From 5a0d5df90ad4096c4d7bdc50ce69cf8673ea6e57 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 30 Apr 2018 18:12:14 +0200 Subject: [PATCH] =?utf8?q?initial=20definition=20of=20=CE=BB=CE=B4=20model?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit + intensional and extensional variant + denotational equivalence this is previously uncommitted matter ported to current version of λδ --- .gitignore | 2 - .../contribs/lambdadelta/apps_2/models/deq.ma | 38 ++++++++++ .../lambdadelta/apps_2/models/model.ma | 39 ++++++++++ .../lambdadelta/apps_2/models/model_li.ma | 73 +++++++++++++++++++ .../lambdadelta/apps_2/models/model_props.ma | 37 ++++++++++ .../lambdadelta/apps_2/models/model_push.ma | 39 ++++++++++ .../contribs/lambdadelta/apps_2/models/veq.ma | 36 +++++++++ .../apps_2/notation/models/at_3.ma | 27 +++++++ .../apps_2/notation/models/inwbrackets_4.ma | 27 +++++++ .../apps_2/notation/models/ringeq_4.ma | 27 +++++++ .../apps_2/notation/models/upspoon_3.ma | 27 +++++++ .../apps_2/notation/models/upspoon_4.ma | 27 +++++++ .../apps_2/notation/models/wbrackets_4.ma | 27 +++++++ matita/matita/predefined_virtuals.ml | 4 +- 14 files changed, 426 insertions(+), 4 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/apps_2/models/deq.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/models/model.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/models/model_push.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/models/veq.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/notation/models/at_3.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/notation/models/inwbrackets_4.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/notation/models/ringeq_4.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/notation/models/upspoon_3.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/notation/models/upspoon_4.ma create mode 100644 matita/matita/contribs/lambdadelta/apps_2/notation/models/wbrackets_4.ma diff --git a/.gitignore b/.gitignore index b782458ea..b6713e390 100644 --- a/.gitignore +++ b/.gitignore @@ -71,8 +71,6 @@ matita/matita/contribs/lambdadelta/.depend matita/matita/contribs/lambdadelta/nodes matita/matita/contribs/lambdadelta/token matita/matita/contribs/lambdadelta/2A1 -matita/matita/contribs/lambdadelta/apps_2/notation -matita/matita/contribs/lambdadelta/apps_2/models matita/matita/contribs/lambdadelta/ground_2/xoa/xoa2.ma matita/matita/contribs/lambdadelta/ground_2/notation/xoa/notation2.ma matita/matita/contribs/lambdadelta/*/*_probe.txt diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/deq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/deq.ma new file mode 100644 index 000000000..a5fa28842 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/deq.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "apps_2/notation/models/ringeq_4.ma". +include "apps_2/models/model_li.ma". +include "apps_2/models/model_props.ma". + +(* DENOTATIONAL EQUIVALENCE ************************************************) + +definition deq (M): relation3 lenv term term ≝ + λL,T1,T2. ∀gv,lv. lv ϵ ⟦L⟧[gv] → ⟦T1⟧[gv, lv] ≗{M} ⟦T2⟧[gv, lv]. + +interpretation "denotational equivalence (model)" + 'RingEq M L T1 T2 = (deq M L T1 T2). + +(* Basic properties *********************************************************) + +lemma deq_refl (M): is_model M → + c_reflexive … (deq M). +/2 width=1 by mq/ qed. +(* +lemma veq_sym: ∀M. symmetric … (veq M). +// qed-. + +theorem veq_trans: ∀M. transitive … (veq M). +// qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/model.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model.ma new file mode 100644 index 000000000..88703cfa2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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_2/notation/relations/ringeq_3.ma". +include "apps_2/notation/models/at_3.ma". +include "apps_2/notation/models/wbrackets_4.ma". +include "basic_2/syntax/term.ma". + +(* MODEL ********************************************************************) + +record model: Type[1] ≝ { + dd: Type[0]; (* denotations domain *) + sq: relation2 dd dd; (* structural equivalence *) + sv: nat → dd; (* sort evaluation *) + ap: dd → dd → dd; (* application *) + ti: (nat → dd) → (nat → dd) → term → dd (* term interperpretation *) +}. + +interpretation "structural equivalence (model)" + 'RingEq M d1 d2 = (sq M d1 d2). + +interpretation "application (model)" + 'At M d1 d2 = (ap M d1 d2). + +interpretation "term interpretation (model)" + 'WBrackets M gv lv T = (ti M gv lv T). + +definition evaluation: model → Type[0] ≝ λM. nat → dd M. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma new file mode 100644 index 000000000..07266f8d3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model_li.ma @@ -0,0 +1,73 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/lenv.ma". +include "apps_2/models/model_push.ma". +include "apps_2/notation/models/inwbrackets_4.ma". + +(* LOCAL ENVIRONMENT INTERPRETATION ****************************************) + +inductive li (M) (gv): relation2 lenv (evaluation M) ≝ +| li_atom: ∀lv. li M gv (⋆) lv +| li_abbr: ∀lv,d,L,V. li M gv L lv → ⟦V⟧[gv, lv] ≗ d → li M gv (L.ⓓV) (⫯[d]lv) +| li_abst: ∀lv,d,L,W. li M gv L lv → li M gv (L.ⓛW) (⫯[d]lv) +| li_unit: ∀lv,d,I,L. li M gv L lv → li M gv (L.ⓤ{I}) (⫯[d]lv) +. + +interpretation "local environment interpretation (model)" + 'InWBrackets M gv L lv = (li M gv L lv). + +(* Basic inversion lemmas ***************************************************) + +fact li_inv_abbr_aux (M) (gv): ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀L,V. Y = L.ⓓV → + ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⟦V⟧{M}[gv, lv] ≗ d & ⫯{M}[d]lv = v. +#M #gv #v #Y * -v -Y +[ #lv #K #W #H destruct +| #lv #d #L #V #HL #HV #K #W #H destruct /2 width=5 by ex3_2_intro/ +| #lv #d #L #V #_ #K #W #H destruct +| #lv #d #I #L #_ #K #W #H destruct +] +qed-. + +lemma li_inv_abbr (M) (gv): ∀v,L,V. v ϵ ⟦L.ⓓV⟧{M}[gv] → + ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⟦V⟧{M}[gv, lv] ≗ d & ⫯{M}[d]lv = v. +/2 width=3 by li_inv_abbr_aux/ qed-. + +fact li_inv_abst_aux (M) (gv): ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀L,W. Y = L.ⓛW → + ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv = v. +#M #gv #v #Y * -v -Y +[ #lv #K #U #H destruct +| #lv #d #L #V #_ #_ #K #U #H destruct +| #lv #d #L #V #HL #K #U #H destruct /2 width=4 by ex2_2_intro/ +| #lv #d #I #L #_ #K #U #H destruct +] +qed-. + +lemma li_inv_abst (M) (gv): ∀v,L,W. v ϵ ⟦L.ⓛW⟧{M}[gv] → + ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv = v. +/2 width=4 by li_inv_abst_aux/ qed-. + +fact li_inv_unit_aux (M) (gv): ∀v,Y. v ϵ ⟦Y⟧{M}[gv] → ∀I,L. Y = L.ⓤ{I} → + ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv = v. +#M #gv #v #Y * -v -Y +[ #lv #J #K #H destruct +| #lv #d #L #V #_ #_ #J #K #H destruct +| #lv #d #L #V #_ #J #K #H destruct +| #lv #d #I #L #HL #J #K #H destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma li_inv_unit (M) (gv): ∀v,I,L. v ϵ ⟦L.ⓤ{I}⟧{M}[gv] → + ∃∃lv,d. lv ϵ ⟦L⟧{M}[gv] & ⫯{M}[d]lv = v. +/2 width=4 by li_inv_unit_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma new file mode 100644 index 000000000..c07d13022 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model_props.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "apps_2/models/model_push.ma". + +(* MODEL ********************************************************************) + +record is_model (M): Prop ≝ { + mq: reflexive … (sq M); + ms: ∀gv,lv,s. ⟦⋆s⟧{M}[gv, lv] ≗ sv M s; + ml: ∀gv,lv,i. ⟦#i⟧{M}[gv, lv] ≗ lv i; + mg: ∀gv,lv,l. ⟦§l⟧{M}[gv, lv] ≗ gv l; + md: ∀gv,lv,p,V,T. ⟦ⓓ{p}V.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[⟦V⟧[gv, lv]]lv]; + mi: ∀gv,lv1,lv2,p,W,T. ⟦W⟧{M}[gv, lv1] ≗ ⟦W⟧{M}[gv, lv2] → + (∀d. ⟦T⟧{M}[gv, ⫯[d]lv1] ≗ ⟦T⟧{M}[gv, ⫯[d]lv2]) → + ⟦ⓛ{p}W.T⟧[gv, lv1] ≗ ⟦ⓛ{p}W.T⟧[gv, lv2]; + ma: ∀gv,lv,V,T. ⟦ⓐV.T⟧{M}[gv, lv] ≗ ⟦V⟧[gv, lv] @ ⟦T⟧[gv, lv]; + me: ∀gv,lv,W,T. ⟦ⓝW.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, lv]; + mb: ∀gv,lv,d,p,W,T. d @ ⟦ⓛ{p}W.T⟧{M}[gv, lv] ≗ ⟦T⟧[gv, ⫯[d]lv] +}. + +record is_extensional (M): Prop ≝ { + mx: ∀gv,lv1,lv2,p,W1,W2,T1,T2. ⟦W1⟧{M}[gv, lv1] ≗ ⟦W2⟧{M}[gv, lv2] → + (∀d. ⟦T1⟧{M}[gv, ⫯[d]lv1] ≗ ⟦T2⟧{M}[gv, ⫯[d]lv2]) → + ⟦ⓛ{p}W1.T1⟧[gv, lv1] ≗ ⟦ⓛ{p}W2.T2⟧[gv, lv2] +}. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/model_push.ma b/matita/matita/contribs/lambdadelta/apps_2/models/model_push.ma new file mode 100644 index 000000000..acf96a0cc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/model_push.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "apps_2/notation/models/upspoon_4.ma". +include "apps_2/notation/models/upspoon_3.ma". +include "apps_2/models/model.ma". + +(* MODEL ********************************************************************) + +definition push (M): nat → dd M → evaluation M → evaluation M ≝ + λj,d,lv,i. tri … i j (lv i) d (lv (↓i)). + +interpretation "generic push (model evaluation)" + 'UpSpoon M i d lv = (push M i d lv). + +interpretation "push (model evaluation)" + 'UpSpoon M d lv = (push M O d lv). + +(* Basic properties *********************************************************) + +lemma push_lt: ∀M,lv,d,j,i. i < j → (⫯{M}[j←d] lv) i = lv i. +/2 width=1 by tri_lt/ qed-. + +lemma push_eq: ∀M,lv,d,i. (⫯{M}[i←d] lv) i = d. +/2 width=1 by tri_eq/ qed-. + +lemma push_gt: ∀M,lv,d,j,i. j < i → (⫯{M}[j←d] lv) i = lv (↓i). +/2 width=1 by tri_gt/ qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma new file mode 100644 index 000000000..a64dc2b19 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "apps_2/models/model_props.ma". + +(* EVALUATION EQUIVALENCE **************************************************) + +definition veq (M): relation (evaluation M) ≝ + λv1,v2. ∀d. v1 d ≗ v2 d. + +interpretation "evaluation equivalence (model)" + 'RingEq M v1 v2 = (veq M v1 v2). + +(* Basic properties *********************************************************) + +lemma veq_refl (M): is_model M → + reflexive … (veq M). +/2 width=1 by mq/ qed. +(* +lemma veq_sym: ∀M. symmetric … (veq M). +// qed-. + +theorem veq_trans: ∀M. transitive … (veq M). +// qed-. +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/at_3.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/at_3.ma new file mode 100644 index 000000000..a6530327c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/notation/models/at_3.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "models" COMPONENT **************************************) + +notation < "hvbox( d1 @ break d2 )" + right associative with precedence 47 + for @{ 'At $M $d1 $d2 }. + +notation > "hvbox( d1 @ break d2 )" + right associative with precedence 47 + for @{ 'At ? $d1 $d2 }. + +notation > "hvbox( d1 @{ break term 46 M } break term 46 d2 )" + non associative with precedence 47 + for @{ 'At $M $d1 $d2 }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/inwbrackets_4.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/inwbrackets_4.ma new file mode 100644 index 000000000..ed01d0915 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/notation/models/inwbrackets_4.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "models" COMPONENT **************************************) + +notation < "hvbox( lv ϵ ⟦ break term 46 L ⟧[ break term 46 gv ] )" + non associative with precedence 45 + for @{ 'InWBrackets $M $gv $L $lv }. + +notation > "hvbox( lv ϵ ⟦ break term 46 L ⟧[ break term 46 gv ] )" + non associative with precedence 45 + for @{ 'InWBrackets ? $gv $L $lv }. + +notation > "hvbox( lv ϵ ⟦ break term 46 L ⟧{ break term 46 M }[ break term 46 gv ] )" + non associative with precedence 45 + for @{ 'InWBrackets $M $gv $L $lv }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/ringeq_4.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/ringeq_4.ma new file mode 100644 index 000000000..bb6c30068 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/notation/models/ringeq_4.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation < "hvbox( L ⊢ break term 46 T1 ≗ break term 46 T2 )" + non associative with precedence 45 + for @{ 'RingEq $M $L $T1 $T2 }. + +notation > "hvbox( L ⊢ break term 46 T1 ≗ break term 46 T2 )" + non associative with precedence 45 + for @{ 'RingEq ? $L $T1 $T2 }. + +notation > "hvbox( L ⊢ break term 46 T1 ≗{ break term 46 M } break term 46 T2 )" + non associative with precedence 45 + for @{ 'RingEq $M $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/upspoon_3.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/upspoon_3.ma new file mode 100644 index 000000000..a12cbbfb3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/notation/models/upspoon_3.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "models" COMPONENT **************************************) + +notation < "hvbox( ⫯[ break term 46 d ] break term 46 lv )" + non associative with precedence 46 + for @{ 'UpSpoon $M $d $lv }. + +notation > "hvbox( ⫯[ break term 46 d ] break term 46 lv )" + non associative with precedence 46 + for @{ 'UpSpoon ? $d $lv }. + +notation > "hvbox( ⫯{ term 46 M }[ break term 46 d ] break term 46 lv )" + non associative with precedence 46 + for @{ 'UpSpoon $M $d $lv }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/upspoon_4.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/upspoon_4.ma new file mode 100644 index 000000000..ef10aa2fb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/notation/models/upspoon_4.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "models" COMPONENT **************************************) + +notation < "hvbox( ⫯[ term 46 i ← break term 46 d ] break term 46 lv )" + non associative with precedence 46 + for @{ 'UpSpoon $M $i $d $lv }. + +notation > "hvbox( ⫯[ term 46 i ← break term 46 d ] break term 46 lv )" + non associative with precedence 46 + for @{ 'UpSpoon ? $i $d $lv }. + +notation > "hvbox( ⫯{ term 46 M }[ break term 46 i ← break term 46 d ] break term 46 lv )" + non associative with precedence 46 + for @{ 'UpSpoon $M $i $d $lv }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/wbrackets_4.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/wbrackets_4.ma new file mode 100644 index 000000000..d1df3d59c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/notation/models/wbrackets_4.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "models" COMPONENT **************************************) + +notation < "hvbox( ⟦ term 46 T ⟧[ break term 46 gv, break term 46 lv ] )" + non associative with precedence 75 + for @{ 'WBrackets $M $gv $lv $T }. + +notation > "hvbox( ⟦ term 46 T ⟧[ break term 46 gv, break term 46 lv ] )" + non associative with precedence 75 + for @{ 'WBrackets ? $gv $lv $T }. + +notation > "hvbox( ⟦ term 46 T ⟧{ break term 46 M }[ break term 46 gv , break term 46 lv ] )" + non associative with precedence 75 + for @{ 'WBrackets $M $gv $lv $T }. diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index e7814e5f3..e51f7b54e 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1525,8 +1525,8 @@ let predefined_classes = [ ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ; ["("; "❨"; "❪"; "❲"; "（"; ]; [")"; "❩"; "❫"; "❳"; "）"; ]; - ["["; "⦋"; "〚"; ] ; - ["]"; "⦌"; "〛"; ] ; + ["["; "⦋"; "⟦"; ] ; + ["]"; "⦌"; "⟧"; ] ; ["{"; "❴"; "⦃" ] ; ["}"; "❵"; "⦄" ] ; ["□"; "◽"; "▪"; "◾"; ]; -- 2.39.2