-
- Context
- `(Guest : ProgrammingLanguage)
- `(Host : ProgrammingLanguage)
- (HostMonoidal : MonoidalEnrichment (TypesEnrichedInJudgments Host))
- (HostMonic : MonicEnrichment (TypesEnrichedInJudgments Host)).
-
-Definition TwoLevelLanguage (Guest Host:ProgrammingLanguageSMME)
- := Reification Guest Host (me_i Host).
-
-Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
-| NLevelLanguage_zero : forall lang, NLevelLanguage O lang
-| NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n,
- TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
-
-Definition OmegaLevelLanguage : Type :=
- { f : nat -> ProgrammingLanguageSMME
- & forall n, TwoLevelLanguage (f n) (f (S n)) }.
-