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
data Hiding Source
Constructors
Hidden
NotHidden
data Arg e Source
A function argument can be hidden.
Constructors
Arg
argHiding :: Hiding
unArg :: e
data Named name a Source
Constructors
Named
nameOf :: Maybe name
namedThing :: 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
data Access Source
Access modifier.
Constructors
PrivateAccess
PublicAccess
data IsAbstract Source
Abstract or concrete
Constructors
AbstractDef
ConcreteDef
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
newtype Constr a Source
Constructors
Constr a
Produced by Haddock version 2.6.0