@@ -582,7 +582,7 @@ instance Eq NameType where
582582 _ == _ = False
583583
584584-- | Terms in the core language
585−data TT n = P NameType n (TT n) -- ^ named references
585+data TT n = P NameType n (TT n) -- ^ named references with type
586586 | V Int -- ^ a resolved de Bruijn-indexed variable
587587 | Bind n (Binder (TT n)) (TT n) -- ^ a binding
588588 | App (TT n) (TT n) -- ^ function, function type, arg
@@ -679,6 +679,7 @@ vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc
679679 instancesB _ = 0
680680vinstances i t = 0
681681
682+-- | Replace the outermost (index 0) de Bruijn variable with the given term
682683instantiate :: TT n -> TT n -> TT n
683684instantiate e = subst 0 where
684685 subst i (V x) | i == x = e
@@ -687,6 +688,9 @@ instantiate e = subst 0 where
687688 subst i (Proj x idx) = Proj (subst i x) idx
688689 subst i t = t
689690
691+-- | 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
693+-- that has been substituted.
690694substV :: TT n -> TT n -> TT n
691695substV x tm = dropV 0 (instantiate x tm) where
692696 dropV i (V x) | x > i = V (x - 1)