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

Safe HaskellSafe-Infered

Agda.Syntax.Common

Description

Some common syntactic entities are defined in this module.

Synopsis

Documentation

data Relevance Source

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

Constructors

Relevant

the argument is (possibly) relevant at compile-time

NonStrict

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

Irrelevant

the argument is irrelevant at compile- and runtime

Forced

the argument can be skipped during equality checking

moreRelevant :: Relevance -> Relevance -> BoolSource

Information ordering. Relevant moreRelevant Forced moreRelevant NonStrict moreRelevant Irrelevant

data Arg e Source

A function argument can be hidden and/or irrelevant.

Constructors

Arg 

Instances

Functor Arg 
Typeable1 Arg 
Foldable Arg 
Traversable Arg 
Abstract Telescope 
KillVar Telescope 
GenC Telescope 
EmbPrj Telescope 
PrettyTCM Telescope 
Reduce Telescope 
Instantiate Telescope 
ShrinkC Telescope Telescope 
Reify Telescope Telescope 
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) 
(Reify 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) 
DotVars a => DotVars (Arg a) 
MentionsMeta t => MentionsMeta (Arg t) 
Occurs a => Occurs (Arg a) 
ComputeOccurrences a => ComputeOccurrences (Arg a) 
HasPolarity a => HasPolarity (Arg a) 
Unquote a => Unquote (Arg a) 
StripAllProjections a => StripAllProjections (Arg a) 
LowerMeta a => LowerMeta (Arg a) 
ToConcrete a c => ToConcrete (Arg a) (Arg c) 
ShrinkC a b => ShrinkC (Arg a) (Arg b) 
ToAbstract c a => ToAbstract (Arg c) (Arg a) 
Reify i a => Reify (Arg i) (Arg a) 
SubstHH a b => SubstHH (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.

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

Constructors

InfixDef 
PrefixDef 

data Access Source

Access modifier.

Constructors

PrivateAccess 
PublicAccess 
OnlyQualified

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

data NameId Source

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

Constructors

NameId Nat Integer 

newtype Constr a Source

Constructors

Constr a