module Render.Utils where import Agda.Utils.Time ( CPUTime ) import Agda.Utils.Pretty (pretty) import Render.Class import Render.RichText instance Render CPUTime where render :: CPUTime -> Inlines render = String -> Inlines text (String -> Inlines) -> (CPUTime -> String) -> CPUTime -> Inlines forall b c a. (b -> c) -> (a -> b) -> a -> c . Doc -> String forall a. Show a => a -> String show (Doc -> String) -> (CPUTime -> Doc) -> CPUTime -> String forall b c a. (b -> c) -> (a -> b) -> a -> c . CPUTime -> Doc forall a. Pretty a => a -> Doc pretty