@@ -1173,7 +1173,9 @@ process fn (MakeDoc s) =
11731173process fn (PrintDef n) =
11741174 do ist <- getIState
11751175 let patdefs = idris_patdefs ist
1176− result = map (ppDef ist) (lookupCtxtName n patdefs)
1176+ tyinfo = idris_datatypes ist
1177+ result = map (ppDef ist) (lookupCtxtName n patdefs) ++
1178+ map (ppTy ist) (lookupCtxtName n tyinfo)
11771179 case result of
11781180 [] -> iPrintError "Not found"
11791181 outs -> iRenderResult . vsep $ outs
@@ -1194,6 +1196,16 @@ process fn (PrintDef n) =
11941196 in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)
11951197 ppMissing _ = empty
11961198
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))
1204+ where
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)
11971209
11981210showTotal :: Totality -> IState -> String
11991211showTotal t@(Partial (Other ns)) i