Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




Some common syntactic entities are defined in this module.



data Delayed Source

Used to specify whether something should be delayed.




data Relevance Source

A function argument can be relevant or irrelevant. See Irrelevance.



The argument is (possibly) relevant at compile-time.


The argument may never flow into evaluation position. Therefore, it is irrelevant at run-time. It is treated relevantly during equality checking.


The argument is irrelevant at compile- and runtime.


The argument can be skipped during equality checking because its value is already determined by the type.


The polarity checker has determined that this argument is unused in the definition. It can be skipped during equality checking but should be mined for solutions of meta-variables with relevance UnusedArg

moreRelevant :: Relevance -> Relevance -> BoolSource

Information ordering. Relevant `moreRelevant` UnusedArg `moreRelevant` Forced `moreRelevant` NonStrict `moreRelevant` Irrelevant

Function type domain

data Dom e Source

Similar to Arg, but we need to distinguish an irrelevance annotation in a function domain (the domain itself is not irrelevant!) from an irrelevant argument.

Dom is used in Pi of internal syntax, in Context and Telescope. Arg is used for actual arguments (Var, Con, Def etc.) and in Abstract syntax and other situations.




Argument decoration

data Arg e Source

A function argument can be hidden and/or irrelevant.




Functor Arg 
Typeable1 Arg 
Foldable Arg 
Traversable Arg 
UniverseBi Args Pattern 
UniverseBi Args Term 
Eq a => Eq (Arg a) 
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) 
Subst a => Subst (Arg a) 
AbstractTerm a => AbstractTerm (Arg a) 
(ReifyWhen a e, ToConcrete e c, Pretty c) => PrettyTCM (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) 
MentionsMeta t => MentionsMeta (Arg t) 
EmbPrj a => EmbPrj (Arg a) 
Occurs a => Occurs (Arg a) 
ComputeOccurrences a => ComputeOccurrences (Arg a) 
HasPolarity a => HasPolarity (Arg a) 
Unquote a => Unquote (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) 
ReifyWhen i a => Reify (Arg i) (Arg a)

Skip reification of implicit and irrelevant args if option is off.

Reify i a => Reify (Dom i) (Arg a) 
ReifyWhen i a => ReifyWhen (Arg i) (Arg a) 
SubstHH a b => SubstHH (Arg a) (Arg b) 
ShrinkC a b => ShrinkC (Arg a) (Arg b) 

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.

Named arguments

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) 
(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) 
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named String a) 
(EmbPrj s, EmbPrj t) => EmbPrj (Named s t) 
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) 
Reify i a => Reify (Named n i) (Named n a) 
ReifyWhen i a => ReifyWhen (Named n i) (Named n 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.

namedArg :: NamedArg a -> aSource

Get the content of a NamedArg.

updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg bSource

The functor instance for NamedArg would be ambiguous, so we give it another name here.

Infixity, access, abstract, etc.

data IsInfix Source

Functions can be defined in both infix and prefix style. See LHS.



data Access Source

Access modifier.



Visible from outside, but not exported when opening the module Used for qualified constructors.

type Nat = IntSource

data NameId Source

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


NameId Integer Integer 

newtype Constr a Source


Constr a