]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta.etc
- extended multiple substitutions now uses bounds in ynat (ie. they
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / snta / snta.etc
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : * break [ l ] break term 46 T2 )"
16    non associative with precedence 45
17    for @{ 'NativeTypeStar $h $l $L $T1 $T2 }.
18
19 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : break [ l ] break term 46 T2 )"
20    non associative with precedence 45
21    for @{ 'StratifiedNativeType $h $l $L $T1 $T2 }.
22
23 include "basic_2/static/sh.ma".
24 include "basic_2/equivalence/cpcs.ma".
25
26 (* STRATIFIED NATIVE TYPE ASSIGNMENT ON TERMS *******************************)
27
28 inductive snta (h:sh): nat → lenv → relation term ≝
29 | snta_sort: ∀L,k. snta h 0 L (⋆k) (⋆(next h k))
30 | snta_ldef: ∀L,K,V,W,U,i,l. ⇩[0, i] L ≡ K. ⓓV → snta h l K V W →
31              ⇧[0, i + 1] W ≡ U → snta h l L (#i) U
32 | snta_ldec: ∀L,K,W,V,U,i,l. ⇩[0, i] L ≡ K. ⓛW → snta h l K W V →
33              ⇧[0, i + 1] W ≡ U → snta h (l+1) L (#i) U
34 | snta_bind: ∀I,L,V,W,T,U,l1,l2. snta h l1 L V W → snta h l2 (L. ⓑ{I} V) T U →
35              snta h l2 L (ⓑ{I}V.T) (ⓑ{I}V.U)
36 | snta_appl: ∀L,V,W1,W2,T,U,l1,l2. snta h (l1+1) L V W2 →
37              snta h l2 L (ⓛW1.T) (ⓛW2.U) →
38              snta h l2 L (ⓐV.ⓛW1.T) (ⓐV.ⓛW2.U)
39 | snta_pure: ∀L,V,T,U,W,l. snta h (l+1) L T U → snta h l L (ⓐV.U) W →
40              snta h (l+1) L (ⓐV.T) (ⓐV.U)
41 | snta_cast: ∀L,T,U,W,l1,l2. snta h l2 L T U → snta h l1 L U W →
42              snta h l2 L (ⓝU.T) U
43 | snta_conv: ∀L,T,U1,U2,V2,l. snta h l L T U1 → L ⊢ U1 ⬌* U2 →
44              snta h (l-1) L U2 V2 → snta h l L T U2
45 .
46
47 interpretation "stratified native type assignment (term)"
48    'StratifiedNativeType h l L T U = (snta h l L T U).