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

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)) }.
+