From 92e148ed7a7b0068cf2029537b019a88a7b07d43 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 25 Mar 2011 11:22:04 -0700 Subject: [PATCH] add ToLatex instance for TyCon/TyFun --- src/HaskLiteralsAndTyCons.v | 2 ++ src/HaskProofToLatex.v | 4 ---- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiteralsAndTyCons.v index 0592f3a..a0695d2 100644 --- a/src/HaskLiteralsAndTyCons.v +++ b/src/HaskLiteralsAndTyCons.v @@ -86,6 +86,8 @@ Variable tyConToString : TyCon -> string. Extract Inlined Constant tyCon Variable tyFunToString : TyFun -> string. Extract Inlined Constant tyFunToString => "outputableToString". Instance TyConToString : ToString TyCon := { toString := tyConToString }. Instance TyFunToString : ToString TyFun := { toString := tyFunToString }. +Instance TyConToLatex : ToLatex TyCon := { toLatex := fun x => latex (sanitizeForLatex (toString x)) }. +Instance TyFunToLatex : ToLatex TyCon := { toLatex := fun x => latex (sanitizeForLatex (toString x)) }. Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon". Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon". diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index fab70fe..d99469c 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -27,10 +27,6 @@ Section HaskProofToLatex. Definition FreshM' := FMT freshM. Instance FreshMon' : Monad FreshM' := FMT_Monad freshM. - Instance ToLatexTyCon : ToLatex TyCon. - admit. - Defined. - Fixpoint typeToLatex (needparens:bool){κ}(t:RawHaskType TV κ) {struct t} : FMT freshM Latex := match t with | TVar _ v => return toLatex v -- 1.7.10.4