ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Unquote
Contents
Synopsis
- value agdaTermType
- value agdaTypeType
- value qNameType
- data Dirty
- type UnquoteState
- type UnquoteM
- type UnquoteRes
- value unpackUnquoteM
- value packUnquoteM
- value runUnquoteM
- value liftU1
- value liftU2
- value inOriginalContext
- value isCon
- value isDef
- value reduceQuotedTerm
- class Unquote
- value unquoteN
- value choice
- value ensureDef
- value ensureCon
- value pickName
- value unquoteString
- value unquoteNString
- data ErrorPart
- value renderErrorParts
- value unquoteTCM
- value evalTCM
- type ExeArg
- type StdIn
- type StdOut
- type StdErr
- value requireAllowExec
- value exitCodeToNat
- value tcExec
- PackageAgda-2.8.0.2
- Exports35
- LanguageHaskell2010
- LicenceMIT
- SourceUnquote.hs
Instances26Unquote, …
Unquote QNameDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote ArgInfoDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote HidingDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote MetaIdDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote ModalityDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote QuantityDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote RelevanceDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote BlockerDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote LiteralDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote ClauseDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote ElimDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote PatternDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote SortDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote ErrorPartDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote IntegerDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote BoolDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote CharDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote DoubleDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote Word64Defined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote TextDefined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote a => Unquote (Arg a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote a => Unquote (Dom a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote a => Unquote (Abs a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.UnquoteUnquote a => Unquote [a]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote(Unquote a, Unquote b) => Unquote (a, b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Unquote
Unquote an Arg Term assuming the ArgInfo does not contain information.
(This means, it should be visible, relevant, etc., like defaultArg).
We do a little bit of work here to make it possible to generate nice layout for multi-line error messages. Specifically we split the parts into lines (indicated by n in a string part) and vcat all the lines.
Argument should be a term of type Term → TCM A for some A. Returns the
resulting term of type A. The second argument is the term for the hole,
which will typically be a metavariable. This is passed to the computation
(quoted).
Trusted executables
Raise an error if the --allow-exec option was not specified.
Convert an ExitCode to an Agda natural number.
Call a trusted executable with the given arguments and input.
Returns the exit code, stdout, and stderr.