From 93b1553e602360ffcae3f2670ec3ac189a5e5df9 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 25 Mar 2011 10:07:38 -0700 Subject: [PATCH] add kindToLatex in HaskKinds --- src/HaskKinds.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) 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. -- 1.7.10.4