Agda-2.2.6: A dependently typed functional programming language and proof assistant

Agda.Syntax.Common

Description

Some common syntactic entities are defined in this module.

Synopsis

Documentation

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 

data NameId Source

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

Constructors

NameId Nat Integer