@@ -590,6 +590,8 @@ instance Eq NameType where
590590-- identifiers used for bindings and explicit named references;
591591-- usually we use @TT 'Name'@.
592592data TT n = P NameType n (TT n) -- ^ named references with type
593+ -- (P for "Parameter", motivated by McKinna and Pollack's
594+ -- Pure Type Systems Formalized)
593595 | V Int -- ^ a resolved de Bruijn-indexed variable
594596 | Bind n (Binder (TT n)) (TT n) -- ^ a binding
595597 | App (TT n) (TT n) -- ^ function, function type, arg