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



Some common syntactic entities are defined in this module.



data Relevance Source

A function argument can be relevant or irrelevant.



the argument is (possibly) relevant at compile-time


the argument is irrelevant at compile- and runtime


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




Functor Arg 
Typeable1 Arg 
Foldable Arg 
Traversable Arg 
Eq a => Eq (Arg a) 
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) 

hide :: 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




nameOf :: Maybe name
namedThing :: a


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.



data NameId Source

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


NameId Nat Integer 

newtype Constr a Source


Constr a