Agda-2.2.10: 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 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
= 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 Relevance Source
A function argument can be relevant or irrelevant.
Constructors
Relevantthe argument is (possibly) relevant at compile-time
Irrelevantthe argument is irrelevant at compile- and runtime
Forcedthe argument can be skipped during equality checking
ignoreForced :: Relevance -> RelevanceSource
For comparing Relevance ignoring Forced.
irrelevant :: Bool -> RelevanceSource
Relevance from Bool.
data Arg e Source
A function argument can be hidden and/or irrelevant.
Constructors
Arg
argHiding :: Hiding
argRelevance :: Relevance
unArg :: e
hide :: Arg a -> Arg aSource
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 withArgsFrom args translates xs 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.

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.1