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*)
Notation "'★'" := KindStar.
Notation "a ⇛ b" := (KindArrow a b).
-Fixpoint kindToLatex (k:Kind) : Latex :=
+(* the kind of environment classifiers *)
+Definition ECKind := ★ ⇛ ★ ⇛ ★.
+Opaque ECKind.
+
+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.