X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskKinds.v;h=b61ed0752aac28ba04e694ac19bbd889d8d90c8f;hp=54a1f64459375759e49cbf6d13edd7719ed05f2d;hb=9adf3f5756893322d0114f89c0908590817eda2b;hpb=3d56944e3882ec751fa99b4476a013c4d86fd0f8

diff --git a/src/HaskKinds.v b/src/HaskKinds.v
index 54a1f64..b61ed07 100644
--- a/src/HaskKinds.v
+++ b/src/HaskKinds.v
@@ -38,6 +38,18 @@ Instance KindToString : ToString Kind := { toString := kindToString }.
 Notation "'★'"   := KindStar.
 Notation "a ⇛ b" := (KindArrow a b).
 
+Fixpoint kindToLatexMath (k:Kind) : LatexMath :=
+  match k with
+  | ★                            => rawLatexMath "\star"
+  | ★  ⇛ k2                      => (rawLatexMath "\star\Rightarrow ")+++kindToLatexMath k2
+  | k1 ⇛ k2                      => (rawLatexMath "(")+++kindToLatexMath k1+++(rawLatexMath ")\Rightarrow ")+++kindToLatexMath k2
+  | KindUnliftedType             => rawLatexMath "\text{\tt{\#}}"
+  | KindUnboxedTuple             => rawLatexMath "\text{\tt{(\#)}}"
+  | KindArgType                  => rawLatexMath "\text{\tt{??}}"
+  | KindOpenType                 => rawLatexMath "\text{\tt{?}}"
+  end.
+Instance KindToLatexMath : ToLatexMath Kind := { toLatexMath := kindToLatexMath }.
+
 Instance KindEqDecidable : EqDecidable Kind.
   apply Build_EqDecidable.
   induction v1.