@@ -697,37 +697,37 @@ updateNs ns t = mapPT updateRef t
697data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
697data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
699-- | High level language terms
699-- | High level language terms
700−data PTerm = PQuote Raw
700+data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
701− | PRef FC Name
701+ | PRef FC Name -- ^ A reference to a variable
702 | PInferRef FC Name -- ^ A name to be defined later
702 | PInferRef FC Name -- ^ A name to be defined later
703− | PPatvar FC Name
703+ | PPatvar FC Name -- ^ A pattern variable
704− | PLam Name PTerm PTerm
704+ | PLam Name PTerm PTerm -- ^ A lambda abstraction
705 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
705 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
706− | PLet Name PTerm PTerm PTerm
706+ | PLet Name PTerm PTerm PTerm -- ^ A let binding
707 | PTyped PTerm PTerm -- ^ Term with explicit type
707 | PTyped PTerm PTerm -- ^ Term with explicit type
708 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
708 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
709 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
709 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
710 | PMatchApp FC Name -- ^ Make an application by type matching
710 | 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
712 | PTrue FC PunInfo -- ^ Unit type..?
712 | PTrue FC PunInfo -- ^ Unit type..?
713 | PFalse FC -- ^ _|_
713 | PFalse FC -- ^ _|_
714− | PRefl FC PTerm
714+ | PRefl FC PTerm -- ^ The canonical proof of the equality type
715− | PResolveTC FC
715+ | PResolveTC FC -- ^ Solve this dictionary by type class resolution
716 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
716 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
717− | PRewrite FC PTerm PTerm (Maybe PTerm)
717+ | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
718− | PPair FC PunInfo PTerm PTerm
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
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
720+ | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
721 | PHidden PTerm -- ^ Irrelevant or hidden pattern
721 | PHidden PTerm -- ^ Irrelevant or hidden pattern
722 | PType -- ^ 'Type' type
722 | PType -- ^ 'Type' type
723 | PUniverse Universe -- ^ Some universe
723 | PUniverse Universe -- ^ Some universe
724− | PGoal FC PTerm Name PTerm
724+ | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
725 | PConstant Const -- ^ Builtin types
725 | PConstant Const -- ^ Builtin types
726− | Placeholder
726+ | Placeholder -- ^ Underscore
727− | PDoBlock [PDo]
727+ | PDoBlock [PDo] -- ^ Do notation
728− | PIdiom FC PTerm
728+ | PIdiom FC PTerm -- ^ Idiom brackets
729 | PReturn FC
729 | PReturn FC
730− | PMetavar Name
730+ | PMetavar Name -- ^ A metavariable, ?name
731 | PProof [PTactic] -- ^ Proof script
731 | PProof [PTactic] -- ^ Proof script
732 | PTactics [PTactic] -- ^ As PProof, but no auto solving
732 | PTactics [PTactic] -- ^ As PProof, but no auto solving
733 | PElabError Err -- ^ Error to report on elaboration
733 | PElabError Err -- ^ Error to report on elaboration