@@ -297,7 +297,7 @@ showCG NErased = "_"
297297type Ctxt a = Map.Map Name (Map.Map Name a)
298298emptyContext = Map.empty
299299
300−-- |Return True if the argument Name should be interpreted as the name of a
300+-- |Return True if the argument 'Name' should be interpreted as the name of a
301301-- typeclass.
302302tcname (UN ('@':_)) = True
303303tcname (NS n _) = tcname n
@@ -581,7 +581,9 @@ instance Eq NameType where
581581 TCon _ a == TCon _ b = (a == b) -- ignore tag
582582 _ == _ = False
583583
584−-- | Terms in the core language
584+-- | Terms in the core language. The type parameter is the type of
585+-- identifiers used for bindings and explicit named references;
586+-- usually we use @TT 'Name'@.
585587data TT n = P NameType n (TT n) -- ^ named references with type
586588 | V Int -- ^ a resolved de Bruijn-indexed variable
587589 | Bind n (Binder (TT n)) (TT n) -- ^ a binding
@@ -688,7 +690,7 @@ instantiate e = subst 0 where
688690 subst i (Proj x idx) = Proj (subst i x) idx
689691 subst i t = t
690692
691−-- | As `instantiate`, but also decrement the indices of all de Bruijn variables
693+-- | As 'instantiate', but also decrement the indices of all de Bruijn variables
692694-- remaining in the term, so that there are no more references to the variable
693695-- that has been substituted.
694696substV :: TT n -> TT n -> TT n
@@ -711,7 +713,7 @@ explicitNames (App f a) = App (explicitNames f) (explicitNames a)
711713explicitNames (Proj x idx) = Proj (explicitNames x) idx
712714explicitNames t = t
713715
714−-- | Replace references to the given `Name`-like id with references to
716+-- | Replace references to the given 'Name'-like id with references to
715717-- de Bruijn index 0.
716718pToV :: Eq n => n -> TT n -> TT n
717719pToV n = pToV' n 0
@@ -761,8 +763,8 @@ finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
761763finalise (App f a) = App (finalise f) (finalise a)
762764finalise t = t
763765
764−-- | As `instantiate`, but in addition to replacing `V 0`,
765−-- replace references to the given `Name`-like id.
766+-- | As 'instantiate', but in addition to replacing @'V' 0@,
767+-- replace references to the given 'Name'-like id.
766768subst :: Eq n => n {-^ The id to replace -} ->
767769 TT n {-^ The replacement term -} ->
768770 TT n {-^ The term to replace in -} ->