Agda.Syntax.Common

Delayed

data Delayed

Induction

data Induction

Hiding

data Overlappable

data Hiding

data WithHiding a

class LensHiding a

mergeHiding

visible

notVisible

hidden

hide

hideOrKeepInstance

makeInstance

makeInstance'

isOverlappable

isInstance

sameHiding

Relevance

data Big

data Relevance

allRelevances

class LensRelevance a

isRelevant

isIrrelevant

moreRelevant

irrelevant

unusableRelevance

composeRelevance

inverseComposeRelevance

ignoreForced

irrToNonStrict

nonStrictToRel

nonStrictToIrr

Origin of arguments (user-written, inserted or reflected)

data Origin

data WithOrigin a

class LensOrigin a

Argument decoration

data ArgInfo

class LensArgInfo a

defaultArgInfo

Arguments

data Arg e

defaultArg

withArgsFrom

withNamedArgsFrom

Names

class Underscore a

Function type domain

data Dom e

argFromDom

domFromArg

defaultDom

Named arguments

data Named name a

type Named_

unnamed

named

type NamedArg a

namedArg

defaultNamedArg

updateNamedArg

setNamedArg

Range decoration.

data Ranged a

unranged

Raw names (before parsing into name parts).

type RawName

rawNameToString

stringToRawName

type RString

Further constructor and projection info

data ConOrigin

bestConInfo

data ProjOrigin

data DataOrRecord

Infixity, access, abstract, etc.

data IsInfix

data Access

data IsAbstract

data IsInstance

data IsMacro

type Nat

type Arity

NameId

data NameId

Meta variables

data MetaId

data Constr a

Placeholders (used to parse sections)

data PositionInName

data MaybePlaceholder e

noPlaceholder

Interaction meta variables

data InteractionId

Import directive

data ImportDirective' a b

data Using' a b

defaultImportDir

isDefaultImportDir

data ImportedName' a b

setImportedName

data Renaming' a b

HasRange instances

KillRange instances

NFData instances

Termination

data TerminationCheck m

Positivity

type PositivityCheck