|
Agda.Interaction.BasicOps |
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
Parses an expression.
|
|
|
|
|
|
|
|
|
|
|
|
|
Evaluate the given expression in the current environment
|
|
|
|
|
Constructors | AsIs | | Instantiated | | HeadNormal | | Normalised | |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Returns the type of the expression in the current environment
|
|
|
|
|
|
|
|
|
|
|
Runs the given computation as if in an anonymous goal at the end
of the top-level module.
|
|
|
:: Range | The range of the next argument.
| -> String | The module name.
| -> TCM ([Name], [(Name, Type)]) | Module names, names paired up with
corresponding types.
| Returns the contents of the given module.
|
|
|
Produced by Haddock version 2.6.1 |