ModuleAgda-2.7.0.1Haskell2010
Agda.TypeChecking.Unquote
- 9 types
- 1 class
- 28 values
- PackageAgda-2.7.0.1
- Exports38
- LanguageHaskell2010
- LicenceMIT
- SourceUnquote.hs
Instances26Unquote, …
Unquote QNameDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote ArgInfoDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote HidingDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote MetaIdDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote ModalityDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote QuantityDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote RelevanceDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote BlockerDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote LiteralDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote ClauseDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote ElimDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote PatternDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote SortDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote ErrorPartDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote IntegerDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote Word64Defined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote BoolDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote CharDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote DoubleDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote TextDefined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote a => Unquote (Arg a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote a => Unquote (Dom a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote a => Unquote (Abs a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.UnquoteUnquote a => Unquote [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Unquote(Unquote a, Unquote b) => Unquote (a, b)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Unquote
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
10 declarationsRaise 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.
Raise an error if the trusted executable cannot be found.