Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Syntax.Common
Description
Some common syntactic entities are defined in this module.
Synopsis
data Induction
= Inductive
| CoInductive
data Hiding
= Hidden
| NotHidden
data Arg e = Arg {
argHiding :: Hiding
unArg :: e
}
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
= InfixDef
| PrefixDef
data Access
= PrivateAccess
| PublicAccess
data IsAbstract
= AbstractDef
| ConcreteDef
type Nat = Integer
type Arity = Nat
data NameId = NameId Nat Integer
newtype Constr a = Constr a
Documentation
data Induction Source
Constructors
Inductive
CoInductive
show/hide Instances
data Hiding Source
Constructors
Hidden
NotHidden
show/hide Instances
data Arg e Source
A function argument can be hidden.
Constructors
Arg
argHiding :: Hiding
unArg :: e
show/hide Instances
data Named name a Source
Constructors
Named
nameOf :: Maybe name
namedThing :: a
show/hide Instances
Typeable2 Named
Functor (Named name)
Traversable (Named name)
Foldable (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)
unnamed :: a -> Named name aSource
named :: name -> a -> Named name aSource
type NamedArg a = Arg (Named String a)Source
Only Hidden arguments can have names.
data IsInfix Source
Functions can be defined in both infix and prefix style. See Agda.Syntax.Concrete.LHS.
Constructors
InfixDef
PrefixDef
show/hide Instances
data Access Source
Access modifier.
Constructors
PrivateAccess
PublicAccess
show/hide Instances
data IsAbstract Source
Abstract or concrete
Constructors
AbstractDef
ConcreteDef
show/hide Instances
type Nat = IntegerSource
type Arity = NatSource
data NameId Source
The unique identifier of a name. Second argument is the top-level module identifier.
Constructors
NameId Nat Integer
show/hide Instances
newtype Constr a Source
Constructors
Constr a
show/hide Instances
Produced by Haddock version 2.4.2