Some common syntactic entities are defined in this module.
- data Induction
- = Inductive
- | CoInductive
- data Hiding
- data Arg e = Arg {}
- 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 hidden.
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.
Constr a |