@@ -633,26 +633,26 @@ data PTerm = PQuote Raw
633633 | PInferRef FC Name -- ^ A name to be defined later
634634 | PPatvar FC Name
635635 | PLam Name PTerm PTerm
636− | PPi Plicity Name PTerm PTerm
636+ | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
637637 | PLet Name PTerm PTerm PTerm
638638 | PTyped PTerm PTerm -- ^ Term with explicit type
639− | PApp FC PTerm [PArg]
639+ | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
640640 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
641641 | PMatchApp FC Name -- ^ Make an application by type matching
642642 | PCase FC PTerm [(PTerm, PTerm)]
643− | PTrue FC PunInfo
644− | PFalse FC
643+ | PTrue FC PunInfo -- ^ Unit type..?
644+ | PFalse FC -- ^ _|_
645645 | PRefl FC PTerm
646646 | PResolveTC FC
647− | PEq FC PTerm PTerm
647+ | PEq FC PTerm PTerm -- ^ Equality type: A = B
648648 | PRewrite FC PTerm PTerm (Maybe PTerm)
649649 | PPair FC PunInfo PTerm PTerm
650650 | PDPair FC PunInfo PTerm PTerm PTerm
651651 | PAlternative Bool [PTerm] -- True if only one may work
652652 | PHidden PTerm -- ^ Irrelevant or hidden pattern
653− | PType
653+ | PType -- ^ 'Type' type
654654 | PGoal FC PTerm Name PTerm
655− | PConstant Const
655+ | PConstant Const -- ^ Builtin types
656656 | Placeholder
657657 | PDoBlock [PDo]
658658 | PIdiom FC PTerm