Clarify an initially-confusing point about `Binder`
commit4dbd81680b4905d38d7a0e69de5eeab66ea89271
authorAlyssa Carter <trillionalyssa@gmail.com>
dateTue 14 Jan 2014, 05:10 (13 years ago)
parentc3659af
src/Idris/Core/TT.hs+3
@@ -466,6 +466,9 @@ deriving instance Binary Raw
466466deriving instance NFData Raw
467467!-}
468468
469+-- The type parameter `b` will normally be something like `TT Name` or just
470+-- `Raw`. We do not make a type-level distinction between TT terms that happen
471+-- to be TT types and TT terms that are not TT types.
469472-- | All binding forms are represented in a unform fashion.
470473data Binder b = Lam { binderTy :: b {-^ type annotation for bound variable-}}
471474 | Pi { binderTy :: b }