From aedfbef5ccfe39e661cc309d2ee1c96a5f70dc5a Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Tue, 7 Jan 2014 15:35:41 +0000
Subject: lem homs and type headers

---
 src/type_internal.ml  | 3 +++
 src/type_internal.mli | 6 ++++++
 2 files changed, 9 insertions(+)

(limited to 'src')

diff --git a/src/type_internal.ml b/src/type_internal.ml
index b019624d..bfed90ee 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -81,3 +81,6 @@ let initial_kind_env =
     ("enum", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}; {k=K_Ord} ], {k = K_Typ}) });
     ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } )
   ]
+
+let rec type_eq l t1 t2 = (t2,[])
+let rec type_coerce l t1 t2 = (t2,[])
diff --git a/src/type_internal.mli b/src/type_internal.mli
index fedc5cc4..2e8c3418 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -68,3 +68,9 @@ type nexp_range =
 type tannot = (t * tag * nexp_range list) option
 
 val initial_kind_env : kind Envmap.t
+
+(* type_eq mutates to unify variables, and will raise an exception if two types cannot be equal *)
+val type_eq : Parse_ast.l -> t -> t -> t * nexp_range list
+
+(* type_eq mutates to unify variables, and will raise an exception if the first type cannot be coerced into the second *)
+val type_coerce : Parse_ast.l -> t -> t -> t * nexp_range list
-- 
cgit v1.2.3