Mercurial > cpdt > repo

changeset 180:de33d1ed7c63

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Templatize Extensional
author Adam Chlipala <adamc@hcoop.net>
date Mon, 10 Nov 2008 14:17:26 -0500
parents 8f3fc56b90d4
children ec44782bffdd
files src/Extensional.v
diffstat 1 files changed, 6 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/Extensional.v	Mon Nov 10 14:12:22 2008 -0500
+++ b/src/Extensional.v	Mon Nov 10 14:17:26 2008 -0500
@@ -103,6 +103,7 @@
 
     Definition ExpDenote t (e : Exp t) := expDenote (e _).
 
+(* begin thide *)
     Section exp_equiv.
       Variables var1 var2 : type -> Type.
 
@@ -129,6 +130,7 @@
 
     Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
       exp_equiv nil (E var1) (E var2).
+(* end thide *)
   End Source.
 
   Module CPS.
@@ -257,6 +259,7 @@
 
   Import Source CPS.
 
+(* begin thide *)
   Fixpoint cpsType (t : Source.type) : CPS.type :=
     match t with
       | Nat => Nat%cps
@@ -310,6 +313,7 @@
   Implicit Arguments cpsExp [var t].
   Definition CpsExp (E : Exp Nat) : Prog :=
     fun var => cpsExp (E _) (PHalt (var := _)).
+(* end thide *)
 
   Eval compute in CpsExp zero.
   Eval compute in CpsExp one.
@@ -323,6 +327,7 @@
   Eval compute in ProgDenote (CpsExp app_ident).
   Eval compute in ProgDenote (CpsExp app_ident').
 
+(* begin thide *)
   Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop :=
     match t return (Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop) with
       | Nat => fun n1 n2 => n1 = n2
@@ -373,6 +378,7 @@
       generalize (cpsExp_correct (e1 := E _) (e2 := E _)
         (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush.
   Qed.
+(* end thide *)
 
 End STLC.