@@ -582,7 +582,7 @@ instance Eq NameType where
582 _ == _ = False
582 _ == _ = False
584-- | Terms in the core language
584-- | 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
586 | V Int -- ^ a resolved de Bruijn-indexed variable
586 | V Int -- ^ a resolved de Bruijn-indexed variable
587 | Bind n (Binder (TT n)) (TT n) -- ^ a binding
587 | Bind n (Binder (TT n)) (TT n) -- ^ a binding
588 | App (TT n) (TT n) -- ^ function, function type, arg
588 | 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
679 instancesB _ = 0
679 instancesB _ = 0
680vinstances i t = 0
680vinstances i t = 0
682+-- | Replace the outermost (index 0) de Bruijn variable with the given term
682instantiate :: TT n -> TT n -> TT n
683instantiate :: TT n -> TT n -> TT n
683instantiate e = subst 0 where
684instantiate e = subst 0 where
684 subst i (V x) | i == x = e
685 subst i (V x) | i == x = e
@@ -687,6 +688,9 @@ instantiate e = subst 0 where
687 subst i (Proj x idx) = Proj (subst i x) idx
688 subst i (Proj x idx) = Proj (subst i x) idx
688 subst i t = t
689 subst i t = t
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.
690substV :: TT n -> TT n -> TT n
694substV :: TT n -> TT n -> TT n
691substV x tm = dropV 0 (instantiate x tm) where
695substV x tm = dropV 0 (instantiate x tm) where
692 dropV i (V x) | x > i = V (x - 1)
696 dropV i (V x) | x > i = V (x - 1)