diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr index d54322a..8bd2fa9 100644 --- a/lib/Quox/Definition.idr +++ b/lib/Quox/Definition.idr @@ -108,18 +108,10 @@ lookupElim0 = lookupElim export prettyDef : {opts : LayoutOpts} -> Name -> Definition -> Eff Pretty (Doc opts) -prettyDef name (MkDef qty type body _) = withPrec Outer $ do +prettyDef name (MkDef qty type _ _) = withPrec Outer $ do qty <- prettyQty qty.qty dot <- dotD name <- prettyFree name colon <- colonD type <- prettyTerm [<] [<] type - case body.term0 of - Just body => do - equals <- cstD - body <- prettyTerm [<] [<] body - hangDSingle - (sep [hsep [hcat [qty, dot, name], colon], hsep [type, equals]]) - body - Nothing => - pure $ sep [hsep [hcat [qty, dot, name], colon], type] + pure $ sep [hsep [hcat [qty, dot, name], colon], type]