Agda.Syntax.Common

Some common syntactic entities are defined in this module.

Documentation

data Induction

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

Constructors

Hidden

NotHidden

Instances

Eq Hiding

Data Hiding

Ord Hiding

Show Hiding

Typeable Hiding

KillRange Hiding

GenC Hiding

EmbPrj Hiding

ShrinkC Hiding Hiding

data Relevance

A function argument can be relevant or irrelevant.

Constructors

Relevant

the argument is (possibly) relevant at compile-time

Irrelevant

the argument is irrelevant at compile- and runtime

Forced

the argument can be skipped during equality checking

Instances

Eq Relevance

Data Relevance

Ord Relevance

Show Relevance

Typeable Relevance

Pretty Relevance

KillRange Relevance

EmbPrj Relevance

PrettyTCM Relevance

ignoreForced :: Relevance -> Relevance

For comparing Relevance ignoring Forced.

irrelevant :: Bool -> Relevance

Relevance from Bool.

data Arg e

A function argument can be hidden and/or irrelevant.

Constructors

Arg

Fields

argHiding :: Hiding

argRelevance :: Relevance

unArg :: e

Instances

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 a

defaultArg :: a -> Arg a

isHiddenArg :: Arg a -> Bool

makeIrrelevant :: Arg a -> Arg a

makeRelevant :: Arg a -> Arg a

withArgsFrom :: [a] -> [Arg b] -> [Arg a]

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

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 a

named :: name -> a -> Named name a

type NamedArg a = Arg (Named String a)

Only Hidden arguments can have names.

data IsInfix

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

Access modifier.

Constructors

PrivateAccess

PublicAccess

Instances

Eq Access

Data Access

Ord Access

Show Access

Typeable Access

EmbPrj Access

data IsAbstract

Abstract or concrete

Constructors

AbstractDef

ConcreteDef

Instances

Eq IsAbstract

Data IsAbstract

Ord IsAbstract

Show IsAbstract

Typeable IsAbstract

EmbPrj IsAbstract

type Nat = Integer

type Arity = Nat

data NameId

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

Constructors

Constr a

Instances

ToConcrete (Constr Constructor) Declaration