From 08f14526fcc06161f2a6d60e7fa55b0a4474a883 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Tue, 8 May 2018 16:12:58 +0200
Subject: [PATCH] [coq] start working on the coq impl, but stop
---
code/gcbpv.v | 28 +++++++++++-----------------
1 file changed, 11 insertions(+), 17 deletions(-)
diff --git a/code/gcbpv.v b/code/gcbpv.v
index 8768a7c..bbf15e6 100644
--- a/code/gcbpv.v
+++ b/code/gcbpv.v
@@ -13,20 +13,17 @@ Record StCtx X := mkStCtx {
ty : StoupSem S -> X
}.
-Definition cdot X : StCtx X := mkStCtx _ None (fun x => match x with end).
-Definition hstoup Y (B : Y) : StCtx Y := mkStCtx _ One (fun x => match x with tt => B end).
+Definition cdot {X} : StCtx X := mkStCtx _ None (fun x => match x with end).
+Definition hstoup {Y} (B : Y) : StCtx Y := mkStCtx _ One (fun x => match x with tt => B end).
-Inductive Dimension := Top | Bot.
-Definition DCtx := StCtx Dimension.
-
-Inductive VType : DCtx -> Set :=
- VUnit : forall I, VType I
-| VTimes : forall {I} (A A' : VType I), VType I
-| VU : forall {I} (B : CType I), VType I
+Inductive VType : Set :=
+ VUnit : VType
+| VTimes : forall (A A' : VType), VType
+| VU : forall (B : CType), VType
with
-CType : DCtx -> Set :=
-| CTo : forall {I} (A : VType I) (B : CType I), CType I
-| CF : forall {I} (A : VType I), CType I.
+CType : Set :=
+| CTo : forall (A : VType) (B : CType), CType
+| CF : forall (A : VType), CType.
Inductive Vlt : VType -> VType -> Set :=
vrefl : forall A, Vlt A A
@@ -67,6 +64,8 @@ Definition ext (G : VCtx) (A : VType) : VCtx :=
| inr tt => A
end).
+Definition CCtx := StCtx CType.
+
Inductive Value : VCtx -> VType -> Type :=
| var : forall G (x : U G), Value G (vty G x)
| vunit : forall G, Value G VUnit
@@ -101,8 +100,3 @@ Term : VCtx -> CCtx -> CType -> Type :=
Term G Dt B
.
-
-
-
-asdf
- .
\ No newline at end of file
--
GitLab