X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskKinds.v;h=3539e953ab946166f39e094c64d0157a5a4281d8;hp=035778000e3a6cf8e1ccae04a596ef250c451a65;hb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f;hpb=93b1553e602360ffcae3f2670ec3ac189a5e5df9

diff --git a/src/HaskKinds.v b/src/HaskKinds.v
index 0357780..3539e95 100644
--- a/src/HaskKinds.v
+++ b/src/HaskKinds.v
@@ -12,7 +12,6 @@ Variable Note                : Type.                         Extract Inlined Con
 Variable natToString         : nat         -> string.        Extract Inlined Constant natToString => "natToString".
 Instance NatToStringInstance : ToString nat := { toString := natToString }.
 
-(* Figure 7: production κ, ι *)
 Inductive Kind : Type := 
   | KindStar          : Kind                      (* ★  - the kind of coercions and the kind of types inhabited by [boxed] values *)
   | KindArrow         : Kind  -> Kind  -> Kind    (* ⇛  - type-function-space; things of kind X⇛Y are NOT inhabited by expressions*)
@@ -38,17 +37,17 @@ Instance KindToString : ToString Kind := { toString := kindToString }.
 Notation "'★'"   := KindStar.
 Notation "a ⇛ b" := (KindArrow a b).
 
-Fixpoint kindToLatex (k:Kind) : Latex :=
+Fixpoint kindToLatexMath (k:Kind) : LatexMath :=
   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{?}}"
+  | ★                            => 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 KindToLatex : ToLatex Kind := { toLatex := kindToLatex }.
+Instance KindToLatexMath : ToLatexMath Kind := { toLatexMath := kindToLatexMath }.
 
 Instance KindEqDecidable : EqDecidable Kind.
   apply Build_EqDecidable.