|
|
|
Description |
Some common syntactic entities are defined in this module.
|
|
Synopsis |
|
|
|
Documentation |
|
|
|
|
|
|
|
|
A function argument can be relevant or irrelevant.
| Constructors | Relevant | the argument is (possibly) relevant at compile-time
| Irrelevant | the argument is irrelevant at compile- and runtime
| Forced | the argument can be skipped during equality checking
|
|
|
|
|
For comparing Relevance ignoring Forced.
|
|
|
Relevance from Bool.
|
|
|
A function argument can be hidden and/or irrelevant.
| Constructors | |
|
|
|
|
|
|
|
|
|
|
|
|
|
xs withArgsFrom args translates xs into a list of Args,
using the elements in args to fill in the non-unArg fields.
Precondition: The two lists should have equal length.
|
|
|
Constructors | Named | | nameOf :: Maybe name | | namedThing :: a | |
|
|
|
|
|
|
|
|
|
Only Hidden arguments can have names.
|
|
|
Functions can be defined in both infix and prefix style. See
Agda.Syntax.Concrete.LHS.
| Constructors | |
|
|
|
Access modifier.
| Constructors | PrivateAccess | | PublicAccess | |
|
|
|
|
Abstract or concrete
| Constructors | |
|
|
|
|
|
|
|
The unique identifier of a name. Second argument is the top-level module
identifier.
| Constructors | |
|
|
|
|
|
Produced by Haddock version 2.6.1 |