Instance TyFunToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toString x) }.
Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
Instance TyFunToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toString x) }.
Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".