Documentation

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
GenC Hiding
EmbPrj Hiding
ShrinkC Hiding Hiding

data Arg e Source

A function argument can be hidden.

Constructors

Arg
Fields argHiding :: Hiding unArg :: e

Instances

Functor Arg
Typeable1 Arg
Foldable Arg
Traversable 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)
Free a => Free (Arg a)
TermLike a => TermLike (Arg a)
Strict a => Strict (Arg a)
Raise t => Raise (Arg t)
Subst a => Subst (Arg a)
AbstractTerm a => AbstractTerm (Arg a)
KillVar a => KillVar (Arg a)
GenC a => GenC (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)
LowerMeta a => LowerMeta (Arg a)
ToConcrete a c => ToConcrete (Arg a) (Arg c)
ToAbstract c a => ToAbstract (Arg c) (Arg a)
ShrinkC a b => ShrinkC (Arg a) (Arg b)
Reify i a => Reify (Arg i) (Arg a)

data Named name a Source

Constructors

Named
Fields nameOf :: Maybe name namedThing :: a

Instances

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)

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

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