rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

add prettyDef

Browse source
This commit is contained in:
rhiannon morris 2023-10-15 16:12:43 +02:00
parent 428397f42b
commit 2e9183bc14
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
lib/Quox/Definition.idr
View file

@ -5,6 +5,7 @@ import public Quox.Syntax
import Quox.Displace import Quox.Displace
import public Data.SortedMap import public Data.SortedMap
import public Quox.Loc import public Quox.Loc
import Quox.Pretty
import Control.Eff import Control.Eff
import Decidable.Decidable import Decidable.Decidable
@ -87,3 +88,14 @@ DefsState = StateL DEFS Definitions
public export %inline public export %inline
lookupElim : {d, n : Nat} -> Name -> Universe -> Definitions -> Maybe (Elim d n) lookupElim : {d, n : Nat} -> Name -> Universe -> Definitions -> Maybe (Elim d n)
lookupElim x u defs = toElim !(lookup x defs) u lookupElim x u defs = toElim !(lookup x defs) u
export
prettyDef : {opts : LayoutOpts} -> Name -> Definition -> Eff Pretty (Doc opts)
prettyDef name (MkDef qty type _ _) = withPrec Outer $ do
qty <- prettyQty qty.qty
dot <- dotD
name <- prettyFree name
colon <- colonD
type <- prettyTerm [<] [<] type
pure $ sep [hsep [hcat [qty, dot, name], colon], type]