@@ -697,37 +697,37 @@ updateNs ns t = mapPT updateRef t
697697data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
698698
699699-- | High level language terms
700−data PTerm = PQuote Raw
701− | PRef FC Name
700+data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
701+ | PRef FC Name -- ^ A reference to a variable
702702 | PInferRef FC Name -- ^ A name to be defined later
703− | PPatvar FC Name
704− | PLam Name PTerm PTerm
703+ | PPatvar FC Name -- ^ A pattern variable
704+ | PLam Name PTerm PTerm -- ^ A lambda abstraction
705705 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
706− | PLet Name PTerm PTerm PTerm
706+ | PLet Name PTerm PTerm PTerm -- ^ A let binding
707707 | PTyped PTerm PTerm -- ^ Term with explicit type
708708 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
709709 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
710710 | PMatchApp FC Name -- ^ Make an application by type matching
711− | PCase FC PTerm [(PTerm, PTerm)]
711+ | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
712712 | PTrue FC PunInfo -- ^ Unit type..?
713713 | PFalse FC -- ^ _|_
714− | PRefl FC PTerm
715− | PResolveTC FC
714+ | PRefl FC PTerm -- ^ The canonical proof of the equality type
715+ | PResolveTC FC -- ^ Solve this dictionary by type class resolution
716716 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
717− | PRewrite FC PTerm PTerm (Maybe PTerm)
718− | PPair FC PunInfo PTerm PTerm
719− | PDPair FC PunInfo PTerm PTerm PTerm
720− | PAlternative Bool [PTerm] -- True if only one may work
717+ | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
718+ | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)
719+ | PDPair FC PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration)
720+ | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
721721 | PHidden PTerm -- ^ Irrelevant or hidden pattern
722722 | PType -- ^ 'Type' type
723723 | PUniverse Universe -- ^ Some universe
724− | PGoal FC PTerm Name PTerm
724+ | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
725725 | PConstant Const -- ^ Builtin types
726− | Placeholder
727− | PDoBlock [PDo]
728− | PIdiom FC PTerm
726+ | Placeholder -- ^ Underscore
727+ | PDoBlock [PDo] -- ^ Do notation
728+ | PIdiom FC PTerm -- ^ Idiom brackets
729729 | PReturn FC
730− | PMetavar Name
730+ | PMetavar Name -- ^ A metavariable, ?name
731731 | PProof [PTactic] -- ^ Proof script
732732 | PTactics [PTactic] -- ^ As PProof, but no auto solving
733733 | PElabError Err -- ^ Error to report on elaboration