don't print the rhs of definitions after checking
This commit is contained in:
parent
5977b7225b
commit
3683aec7be
|
@ -108,18 +108,10 @@ lookupElim0 = lookupElim
|
||||||
|
|
||||||
export
|
export
|
||||||
prettyDef : {opts : LayoutOpts} -> Name -> Definition -> Eff Pretty (Doc opts)
|
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
|
qty <- prettyQty qty.qty
|
||||||
dot <- dotD
|
dot <- dotD
|
||||||
name <- prettyFree name
|
name <- prettyFree name
|
||||||
colon <- colonD
|
colon <- colonD
|
||||||
type <- prettyTerm [<] [<] type
|
type <- prettyTerm [<] [<] type
|
||||||
case body.term0 of
|
pure $ sep [hsep [hcat [qty, dot, name], colon], type]
|
||||||
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]
|
|
||||||
|
|
Loading…
Reference in New Issue