+++ /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 "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : * break [ l ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'NativeTypeStar $h $l $L $T1 $T2 }.
-
-notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : break [ l ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'StratifiedNativeType $h $l $L $T1 $T2 }.
-
-include "basic_2/static/sh.ma".
-include "basic_2/equivalence/cpcs.ma".
-
-(* STRATIFIED NATIVE TYPE ASSIGNMENT ON TERMS *******************************)
-
-inductive snta (h:sh): nat → lenv → relation term ≝
-| snta_sort: ∀L,k. snta h 0 L (⋆k) (⋆(next h k))
-| snta_ldef: ∀L,K,V,W,U,i,l. ⇩[0, i] L ≡ K. ⓓV → snta h l K V W →
- ⇧[0, i + 1] W ≡ U → snta h l L (#i) U
-| snta_ldec: ∀L,K,W,V,U,i,l. ⇩[0, i] L ≡ K. ⓛW → snta h l K W V →
- ⇧[0, i + 1] W ≡ U → snta h (l+1) L (#i) U
-| snta_bind: ∀I,L,V,W,T,U,l1,l2. snta h l1 L V W → snta h l2 (L. ⓑ{I} V) T U →
- snta h l2 L (ⓑ{I}V.T) (ⓑ{I}V.U)
-| snta_appl: ∀L,V,W1,W2,T,U,l1,l2. snta h (l1+1) L V W2 →
- snta h l2 L (ⓛW1.T) (ⓛW2.U) →
- snta h l2 L (ⓐV.ⓛW1.T) (ⓐV.ⓛW2.U)
-| snta_pure: ∀L,V,T,U,W,l. snta h (l+1) L T U → snta h l L (ⓐV.U) W →
- snta h (l+1) L (ⓐV.T) (ⓐV.U)
-| snta_cast: ∀L,T,U,W,l1,l2. snta h l2 L T U → snta h l1 L U W →
- snta h l2 L (ⓝU.T) U
-| snta_conv: ∀L,T,U1,U2,V2,l. snta h l L T U1 → L ⊢ U1 ⬌* U2 →
- snta h (l-1) L U2 V2 → snta h l L T U2
-.
-
-interpretation "stratified native type assignment (term)"
- 'StratifiedNativeType h l L T U = (snta h l L T U).