@@ -297,7 +297,7 @@ showCG NErased = "_"
297type Ctxt a = Map.Map Name (Map.Map Name a)
297type Ctxt a = Map.Map Name (Map.Map Name a)
298emptyContext = Map.empty
298emptyContext = Map.empty
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
301-- typeclass.
301-- typeclass.
302tcname (UN ('@':_)) = True
302tcname (UN ('@':_)) = True
303tcname (NS n _) = tcname n
303tcname (NS n _) = tcname n
@@ -581,7 +581,9 @@ instance Eq NameType where
581 TCon _ a == TCon _ b = (a == b) -- ignore tag
581 TCon _ a == TCon _ b = (a == b) -- ignore tag
582 _ == _ = False
582 _ == _ = False
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'@.
585data TT n = P NameType n (TT n) -- ^ named references with type
587data TT n = P NameType n (TT n) -- ^ named references with type
586 | V Int -- ^ a resolved de Bruijn-indexed variable
588 | V Int -- ^ a resolved de Bruijn-indexed variable
587 | Bind n (Binder (TT n)) (TT n) -- ^ a binding
589 | Bind n (Binder (TT n)) (TT n) -- ^ a binding
@@ -688,7 +690,7 @@ instantiate e = subst 0 where
688 subst i (Proj x idx) = Proj (subst i x) idx
690 subst i (Proj x idx) = Proj (subst i x) idx
689 subst i t = t
691 subst i t = t
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
692-- remaining in the term, so that there are no more references to the variable
694-- remaining in the term, so that there are no more references to the variable
693-- that has been substituted.
695-- that has been substituted.
694substV :: TT n -> TT n -> TT n
696substV :: TT n -> TT n -> TT n
@@ -711,7 +713,7 @@ explicitNames (App f a) = App (explicitNames f) (explicitNames a)
711explicitNames (Proj x idx) = Proj (explicitNames x) idx
713explicitNames (Proj x idx) = Proj (explicitNames x) idx
712explicitNames t = t
714explicitNames t = t
714−-- | Replace references to the given `Name`-like id with references to
716+-- | Replace references to the given 'Name'-like id with references to
715-- de Bruijn index 0.
717-- de Bruijn index 0.
716pToV :: Eq n => n -> TT n -> TT n
718pToV :: Eq n => n -> TT n -> TT n
717pToV n = pToV' n 0
719pToV n = pToV' n 0
@@ -761,8 +763,8 @@ finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
761finalise (App f a) = App (finalise f) (finalise a)
763finalise (App f a) = App (finalise f) (finalise a)
762finalise t = t
764finalise t = t
764−-- | As `instantiate`, but in addition to replacing `V 0`,
766+-- | As 'instantiate', but in addition to replacing @'V' 0@,
765−-- replace references to the given `Name`-like id.
767+-- replace references to the given 'Name'-like id.
766subst :: Eq n => n {-^ The id to replace -} ->
768subst :: Eq n => n {-^ The id to replace -} ->
767 TT n {-^ The replacement term -} ->
769 TT n {-^ The replacement term -} ->
768 TT n {-^ The term to replace in -} ->
770 TT n {-^ The term to replace in -} ->