X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongTypes.v;fp=src%2FHaskStrongTypes.v;h=a7bd11a800a1faa132918cef2c30f32bc53da3a8;hp=4740acbd49235cd952d38a0a5892bd9aa942ed66;hb=025c2de2effdd7177ca875998b65f51236c8c7c6;hpb=be7ab3c195d3d5c4e7883b090c68fa56df2b1dcb

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index 4740acb..a7bd11a 100644
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -66,6 +66,9 @@ Section Raw.
   | TVar           : ∀ κ, TV κ                                              -> RawHaskType κ                     (* a        *)
   | TCon           : ∀ tc,                                                     RawHaskType (tyConKind' tc)       (* T        *)
   | TArrow         :                                                           RawHaskType (★ ⇛★ ⇛★ )            (* (->)     *)
+  (*
+  | TKappa         :                                                           RawHaskType (★ ⇛★ ⇛★ )            (* (~~>)    *)
+  *)
   | TCoerc         : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★   -> RawHaskType ★                     (* (+>)     *)
   | TApp           : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁)        -> RawHaskType κ₂  -> RawHaskType κ₁                    (* φ φ      *)
   | TAll           : ∀ κ,                          (TV κ -> RawHaskType ★)  -> RawHaskType ★                     (* ∀a:κ.φ   *)
@@ -111,6 +114,7 @@ Implicit Arguments TApp   [ [TV] [κ₁] [κ₂] ].
 Implicit Arguments TAll   [ [TV] ].
 
 Notation "t1 ---> t2"        := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
+(*Notation "t1 ~~~> t2"        := (fun TV env => (TApp (TApp TKappa (t1 TV env)) (t2 TV env))).*)
 Notation "φ₁ ∼∼ φ₂ ⇒ φ₃"     := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
 
 (* Kind and Coercion Environments *)