@@ -590,6 +590,8 @@ instance Eq NameType where
590-- identifiers used for bindings and explicit named references;
590-- identifiers used for bindings and explicit named references;
591-- usually we use @TT 'Name'@.
591-- usually we use @TT 'Name'@.
592data TT n = P NameType n (TT n) -- ^ named references with type
592data 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)
593 | V Int -- ^ a resolved de Bruijn-indexed variable
595 | V Int -- ^ a resolved de Bruijn-indexed variable
594 | Bind n (Binder (TT n)) (TT n) -- ^ a binding
596 | Bind n (Binder (TT n)) (TT n) -- ^ a binding
595 | App (TT n) (TT n) -- ^ function, function type, arg
597 | App (TT n) (TT n) -- ^ function, function type, arg