| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 |

Instances

Eq Induction
Data Induction
Ord Induction
Show Induction
Typeable Induction
Arbitrary Induction
CoArbitrary Induction
Pretty Induction
KillRange Induction
EmbPrj Induction

data Hiding | Source

Constructors

Hidden |
NotHidden |

Instances

Eq Hiding
Data Hiding
Ord Hiding
Show Hiding
Typeable Hiding
KillRange Hiding
EmbPrj Hiding
GenC Hiding
ShrinkC Hiding Hiding

data Arg e | Source

A function argument can be hidden.
Constructors

Arg |

argHiding :: Hiding |
unArg :: e |

Instances

Functor Arg
Typeable1 Arg
Traversable Arg
Foldable Arg
Eq e => Eq (Arg e)
Data e => Data (Arg e)
Ord e => Ord (Arg e)
Show a => Show (Arg a)
Sized a => Sized (Arg a)
Pretty e => Pretty (Arg e)
KillRange a => KillRange (Arg a)
HasRange a => HasRange (Arg a)
TermLike a => TermLike (Arg a)
Strict a => Strict (Arg a)
Free a => Free (Arg a)
Raise t => Raise (Arg t)
Subst a => Subst (Arg a)
AbstractTerm a => AbstractTerm (Arg a)
EmbPrj a => EmbPrj (Arg a)
InstantiateFull t => InstantiateFull (Arg t)
Normalise t => Normalise (Arg t)
Reduce t => Reduce (Arg t)
Instantiate t => Instantiate (Arg t)
Match a => Match (Arg a)
DotVars a => DotVars (Arg a)
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a)
Occurs a => Occurs (Arg a)
ComputeOccurrences a => ComputeOccurrences (Arg a)
HasPolarity a => HasPolarity (Arg a)
KillVar a => KillVar (Arg a)
GenC a => GenC (Arg a)
LowerMeta a => LowerMeta (Arg a)
ToConcrete a c => ToConcrete (Arg a) (Arg c)
ToAbstract c a => ToAbstract (Arg c) (Arg a)
Reify i a => Reify (Arg i) (Arg a)
ShrinkC a b => ShrinkC (Arg a) (Arg b)

data Named name a | Source

Constructors

Named |

nameOf :: Maybe name |
namedThing :: a |

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 a | Source

named :: name -> a -> Named name a | Source

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 |

Instances

Eq IsInfix
Data IsInfix
Ord IsInfix
Show IsInfix
Typeable IsInfix

data Access | Source

Access modifier.
Constructors

PrivateAccess |
PublicAccess |

Instances

Eq Access
Data Access
Ord Access
Show Access
Typeable Access
EmbPrj Access

data IsAbstract | Source

Abstract or concrete
Constructors

AbstractDef |
ConcreteDef |

Instances

Eq IsAbstract
Data IsAbstract
Ord IsAbstract
Show IsAbstract
Typeable IsAbstract
EmbPrj IsAbstract

type Nat = Integer | Source

type Arity = Nat | Source

data NameId | Source

The unique identifier of a name. Second argument is the top-level module identifier.
Constructors

NameId Nat Integer |

Instances

Enum NameId
Eq NameId
Data NameId
Ord NameId
Show NameId
Typeable NameId
EmbPrj NameId
HasFresh NameId FreshThings

newtype Constr a | Source

Constructors

Constr a |

Instances

ToConcrete (Constr Constructor) Declaration
ToAbstract (Constr NiceDeclaration) Declaration

Produced by Haddock version 2.4.2