@@ -1173,7 +1173,9 @@ process fn (MakeDoc s) =
1173process fn (PrintDef n) =
1173process fn (PrintDef n) =
1174 do ist <- getIState
1174 do ist <- getIState
1175 let patdefs = idris_patdefs ist
1175 let patdefs = idris_patdefs ist
1176+ tyinfo = idris_datatypes ist
1176− result = map (ppDef ist) (lookupCtxtName n patdefs)
1177+ result = map (ppDef ist) (lookupCtxtName n patdefs) ++
1178+ map (ppTy ist) (lookupCtxtName n tyinfo)
1177 case result of
1179 case result of
1178 [] -> iPrintError "Not found"
1180 [] -> iPrintError "Not found"
1179 outs -> iRenderResult . vsep $ outs
1181 outs -> iRenderResult . vsep $ outs
@@ -1194,6 +1196,16 @@ process fn (PrintDef n) =
1194 in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)
1196 in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)
1195 ppMissing _ = empty
1197 ppMissing _ = empty
1199+ ppTy :: IState -> (Name, TypeInfo) -> Doc OutputAnnotation
1200+ ppTy ist (n, TI constructors isCodata _ _ _)
1201+ = kwd key <+> prettyName True True [] n <+> colon <+>
1202+ align (pprintDelabTy ist n) <+> kwd "where" <$>
1203+ indent 2 (vsep (map (ppCon ist) constructors))
1205+ key | isCodata = "codata"
1206+ | otherwise = "data"
1207+ kwd = annotate AnnKeyword . text
1208+ ppCon ist n = prettyName True False [] n <+> colon <+> align (pprintDelabTy ist n)
1198showTotal :: Totality -> IState -> String
1210showTotal :: Totality -> IState -> String
1199showTotal t@(Partial (Other ns)) i
1211showTotal t@(Partial (Other ns)) i