@@ -700,6 +700,8 @@ substV x tm = dropV 0 (instantiate x tm) where
700700 dropV i (Proj x idx) = Proj (dropV i x) idx
701701 dropV i t = t
702702
703+-- | Replace all non-free de Bruijn references in the given term with references
704+-- to the name of their binding.
703705explicitNames :: TT n -> TT n
704706explicitNames (Bind x b sc) = let b' = fmap explicitNames b in
705707 Bind x b'
@@ -709,6 +711,8 @@ explicitNames (App f a) = App (explicitNames f) (explicitNames a)
709711explicitNames (Proj x idx) = Proj (explicitNames x) idx
710712explicitNames t = t
711713
714+-- | Replace references to the given `Name`-like id with references to
715+-- de Bruijn index 0.
712716pToV :: Eq n => n -> TT n -> TT n
713717pToV n = pToV' n 0
714718pToV' n i (P _ x _) | n == x = V i
@@ -738,6 +742,9 @@ pToVs ns tm = pToVs' ns tm 0 where
738742 pToVs' [] tm i = tm
739743 pToVs' (n:ns) tm i = pToV' n i (pToVs' ns tm (i+1))
740744
745+-- | Replace de Bruijn indices in the given term with explicit references to
746+-- the names of the bindings they refer to. It is an error if the given term
747+-- contains free de Bruijn indices.
741748vToP :: TT n -> TT n
742749vToP = vToP' [] where
743750 vToP' env (V i) = let (n, b) = (env !! i) in
@@ -747,12 +754,19 @@ vToP = vToP' [] where
747754 vToP' env (App f a) = App (vToP' env f) (vToP' env a)
748755 vToP' env t = t
749756
757+-- | Replace every non-free reference to the name of a binding in
758+-- the given term with a de Bruijn index.
750759finalise :: Eq n => TT n -> TT n
751760finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
752761finalise (App f a) = App (finalise f) (finalise a)
753762finalise t = t
754763
755−subst :: Eq n => n -> TT n -> TT n -> TT n
764+-- | As `instantiate`, but in addition to replacing `V 0`,
765+-- replace references to the given `Name`-like id.
766+subst :: Eq n => n {-^ The id to replace -} ->
767+ TT n {-^ The replacement term -} ->
768+ TT n {-^ The term to replace in -} ->
769+ TT n
756770subst n v tm = instantiate v (pToV n tm)
757771
758772substNames :: Eq n => [(n, TT n)] -> TT n -> TT n