From 3683aec7becd6f565b12dae159ff72f6ae9bfddd Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sat, 21 Oct 2023 20:44:27 +0200 Subject: [PATCH] don't print the rhs of definitions after checking --- lib/Quox/Definition.idr | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) 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]