@@ -633,26 +633,26 @@ data PTerm = PQuote Raw
633 | PInferRef FC Name -- ^ A name to be defined later
633 | PInferRef FC Name -- ^ A name to be defined later
634 | PPatvar FC Name
634 | PPatvar FC Name
635 | PLam Name PTerm PTerm
635 | PLam Name PTerm PTerm
636− | PPi Plicity Name PTerm PTerm
636+ | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
637 | PLet Name PTerm PTerm PTerm
637 | PLet Name PTerm PTerm PTerm
638 | PTyped PTerm PTerm -- ^ Term with explicit type
638 | PTyped PTerm PTerm -- ^ Term with explicit type
639− | PApp FC PTerm [PArg]
639+ | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
640 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
640 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
641 | PMatchApp FC Name -- ^ Make an application by type matching
641 | PMatchApp FC Name -- ^ Make an application by type matching
642 | PCase FC PTerm [(PTerm, PTerm)]
642 | PCase FC PTerm [(PTerm, PTerm)]
643− | PTrue FC PunInfo
643+ | PTrue FC PunInfo -- ^ Unit type..?
644− | PFalse FC
644+ | PFalse FC -- ^ _|_
645 | PRefl FC PTerm
645 | PRefl FC PTerm
646 | PResolveTC FC
646 | PResolveTC FC
647− | PEq FC PTerm PTerm
647+ | PEq FC PTerm PTerm -- ^ Equality type: A = B
648 | PRewrite FC PTerm PTerm (Maybe PTerm)
648 | PRewrite FC PTerm PTerm (Maybe PTerm)
649 | PPair FC PunInfo PTerm PTerm
649 | PPair FC PunInfo PTerm PTerm
650 | PDPair FC PunInfo PTerm PTerm PTerm
650 | PDPair FC PunInfo PTerm PTerm PTerm
651 | PAlternative Bool [PTerm] -- True if only one may work
651 | PAlternative Bool [PTerm] -- True if only one may work
652 | PHidden PTerm -- ^ Irrelevant or hidden pattern
652 | PHidden PTerm -- ^ Irrelevant or hidden pattern
653− | PType
653+ | PType -- ^ 'Type' type
654 | PGoal FC PTerm Name PTerm
654 | PGoal FC PTerm Name PTerm
655− | PConstant Const
655+ | PConstant Const -- ^ Builtin types
656 | Placeholder
656 | Placeholder
657 | PDoBlock [PDo]
657 | PDoBlock [PDo]
658 | PIdiom FC PTerm
658 | PIdiom FC PTerm