diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
index 030584c..677f856 100644
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@@ -5,6 +5,7 @@ import public Quox.Syntax
 import Quox.Displace
 import public Data.SortedMap
 import public Quox.Loc
+import Quox.Pretty
 import Control.Eff
 import Decidable.Decidable
 
@@ -87,3 +88,14 @@ DefsState = StateL DEFS Definitions
 public export %inline
 lookupElim : {d, n : Nat} -> Name -> Universe -> Definitions -> Maybe (Elim d n)
 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]