X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FProgrammingLanguageReification.v;h=ab8bb90c5fd62a071f60e1a0eb009aa5904827b4;hp=589f7486749ae860b3ec0d2891187add896b2607;hb=e68b13536be2d1def208bde68dbbcdc4c1097d16;hpb=a8f78bbf37853e3cd5ae5c57efd27e857a0a5249

diff --git a/src/ProgrammingLanguageReification.v b/src/ProgrammingLanguageReification.v
index 589f748..ab8bb90 100644
--- a/src/ProgrammingLanguageReification.v
+++ b/src/ProgrammingLanguageReification.v
@@ -29,6 +29,9 @@ Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
 Require Import ProgrammingLanguage.
 
+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,
@@ -37,3 +40,4 @@ Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
 Definition OmegaLevelLanguage : Type :=
   { f : nat -> ProgrammingLanguageSMME
   & forall n, TwoLevelLanguage (f n) (f (S n)) }.
+