Agda.Syntax.Common
Description
Some common syntactic entities are defined in this module.
- data Induction
- = Inductive
- | CoInductive
- data Hiding
- data Relevance
- = Relevant
- | Irrelevant
- | Forced
- ignoreForced :: Relevance -> Relevance
- irrelevant :: Bool -> Relevance
- data Arg e = Arg {
- argHiding :: Hiding
- argRelevance :: Relevance
- unArg :: e
- hide :: Arg a -> Arg a
- defaultArg :: a -> Arg a
- isHiddenArg :: Arg a -> Bool
- makeIrrelevant :: Arg a -> Arg a
- makeRelevant :: Arg a -> Arg a
- withArgsFrom :: [a] -> [Arg b] -> [Arg a]
- data Named name a = Named {
- nameOf :: Maybe name
- namedThing :: a
- unnamed :: a -> Named name a
- named :: name -> a -> Named name a
- type NamedArg a = Arg (Named String a)
- data IsInfix
- data Access
- data IsAbstract
- type Nat = Integer
- type Arity = Nat
- data NameId = NameId Nat Integer
- newtype Constr a = Constr a
Documentation
Constructors
| Inductive | |
| CoInductive |
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 |
ignoreForced :: Relevance -> RelevanceSource
For comparing Relevance ignoring Forced.
irrelevant :: Bool -> RelevanceSource
Relevance from Bool.
A function argument can be hidden and/or irrelevant.
defaultArg :: a -> Arg aSource
isHiddenArg :: Arg a -> BoolSource
makeIrrelevant :: Arg a -> Arg aSource
makeRelevant :: Arg a -> Arg aSource
withArgsFrom :: [a] -> [Arg b] -> [Arg a]Source
xs translates withArgsFrom argsxs 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.
Functions can be defined in both infix and prefix style. See
Agda.Syntax.Concrete.LHS.
The unique identifier of a name. Second argument is the top-level module identifier.