projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
proofs that Types/Judgments form an enrichment
[coq-hetmet.git]
/
src
/
HaskStrongCategory.v
diff --git
a/src/HaskStrongCategory.v
b/src/HaskStrongCategory.v
index
99772c7
..
abbdc72
100644
(file)
--- a/
src/HaskStrongCategory.v
+++ b/
src/HaskStrongCategory.v
@@
-1,7
+1,7
@@
(*********************************************************************************************************************************)
(* HaskStrongCategory: *)
(* *)
(*********************************************************************************************************************************)
(* HaskStrongCategory: *)
(* *)
-(* Well-typed Haskell terms in a specific tyvar/covar context form a category *)
+(* Well-typed Haskell terms in a specific tyvar/covar context form a category: Types(Haskell) *)
(* *)
(*********************************************************************************************************************************)
(* *)
(*********************************************************************************************************************************)
@@
-17,16
+17,15
@@
Require Import HaskLiteralsAndTyCons.
Require Import HaskStrongTypes.
Require Import HaskStrong.
Require Import HaskStrongTypes.
Require Import HaskStrong.
+(* the category of flat Haskell terms in a specific Γ Δ context *)
(*
(*
- (* the category of flat Haskell terms (n-ary) *)
- Section HaskFlat.
-
- Context (past:@Past V).
+Section HaskFlat.
+ Context (Γ:TypeEnv)(Δ:CoercionEnv Γ).
- Lemma idmor a : [] ~~{SystemFC_Cat_Flat past}~~> [(a,a)].
- (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*)
- admit.
- Defined.
+ Lemma idmor a : [] ~~{SystemFC_Cat_Flat past}~~> [(a,a)].
+ (*set (@nd_rule _ Rule (RVar Γ a past)) as q.*)
+ admit.
+ Defined.
Lemma compmor a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat_Flat past}~~> [(a,c)].
admit.
Lemma compmor a b c : [(a,b)],,[(b,c)] ~~{SystemFC_Cat_Flat past}~~> [(a,c)].
admit.
@@
-125,3
+124,4
@@
Require Import HaskStrong.
*)
*)
+