formatting
authorAdam Megacz <megacz@cs.berkeley.edu>
Tue, 15 Mar 2011 01:50:20 +0000 (18:50 -0700)
committerAdam Megacz <megacz@cs.berkeley.edu>
Tue, 15 Mar 2011 01:50:20 +0000 (18:50 -0700)
src/HaskProofToLatex.v

index be5cb31..25e2523 100644 (file)
@@ -26,9 +26,9 @@ Section ToLatex.
 
   Fixpoint kind2latex (k:Kind) : string :=
     match k with
-    | KindStar                     => "\star"
-    | KindArrow KindStar k2 => "\star\Rightarrow "+++kind2latex k2
-    | KindArrow k1 k2       => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
+    | ★                            => "\star"
+    | ★  ⇛ k2                      => "\star\Rightarrow "+++kind2latex k2
+    | k1 ⇛ k2                      => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
     | KindUnliftedType             => "\text{\tt{\#}}"
     | KindUnboxedTuple             => "\text{\tt{(\#)}}"
     | KindArgType                  => "\text{\tt{??}}"