From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Fri, 25 Mar 2011 17:07:38 +0000 (-0700)
Subject: add kindToLatex in HaskKinds
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=93b1553e602360ffcae3f2670ec3ac189a5e5df9

add kindToLatex in HaskKinds
---

diff --git a/src/HaskKinds.v b/src/HaskKinds.v
index 54a1f64..0357780 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 kindToLatex (k:Kind) : Latex :=
+  match k with
+  | ★                            => latex "\star"
+  | ★  ⇛ k2                      => (latex "\star\Rightarrow ")+=+kindToLatex k2
+  | k1 ⇛ k2                      => (latex "(")+=+kindToLatex k1+=+(latex ")\Rightarrow ")+=+kindToLatex k2
+  | KindUnliftedType             => latex "\text{\tt{\#}}"
+  | KindUnboxedTuple             => latex "\text{\tt{(\#)}}"
+  | KindArgType                  => latex "\text{\tt{??}}"
+  | KindOpenType                 => latex "\text{\tt{?}}"
+  end.
+Instance KindToLatex : ToLatex Kind := { toLatex := kindToLatex }.
+
 Instance KindEqDecidable : EqDecidable Kind.
   apply Build_EqDecidable.
   induction v1.