Some common syntactic entities are defined in this module.
- data Induction
- = Inductive
- | CoInductive
- data Hiding
- data Relevance
- = Relevant
- | Irrelevant
- | Forced
- ignoreForced :: Relevance -> 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
A function argument can be relevant or irrelevant.
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
.
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 Arg
s,
using the elements in args
to fill in the non-unArg
fields.
Precondition: The two lists should have equal length.
Named | |
|
Typeable2 Named | |
Functor (Named name) | |
Foldable (Named name) | |
Traversable (Named name) | |
(Eq name, Eq a) => Eq (Named name a) | |
(Data name, Data a) => Data (Named name a) | |
(Ord name, Ord a) => Ord (Named name a) | |
Show a => Show (Named String a) | |
Sized a => Sized (Named name a) | |
Pretty e => Pretty (Named String e) | |
KillRange a => KillRange (Named name a) | |
HasRange a => HasRange (Named name a) | |
DotVars a => DotVars (Named s a) | |
LowerMeta a => LowerMeta (Named name a) | |
ToConcrete a c => ToConcrete (Named name a) (Named name c) | |
ToAbstract c a => ToAbstract (Named name c) (Named name a) |
Functions can be defined in both infix and prefix style. See
Agda.Syntax.Concrete.LHS
.
Access modifier.
data IsAbstract Source
Abstract or concrete
The unique identifier of a name. Second argument is the top-level module identifier.