X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskLiteralsAndTyCons.v;h=1b8494f3badf03a8e38d4c9b49dd1124e163f6f7;hp=0592f3abbdc1beb8dd823f467c56ace10dbcde4a;hb=edb3cf289c051e99b3c0c1db229ad2d819450e3a;hpb=94d7c55025f5df750ce213172c5d2441b5a210e1 diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiteralsAndTyCons.v index 0592f3a..1b8494f 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 => toLatex (toString x) }. +Instance TyFunToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toString x) }. Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon". Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".