Agda.Syntax.Internal

type Color

type ArgInfo

type Arg a

type Dom a

type NamedArg a

type Args

type NamedArgs

data ConHead

class LensConName a

data Term

data Elim' a

type Elim

type Elims

type ArgName

argNameToString

stringToArgName

appendArgNames

nameToArgName

data Abs a

data Type' a

type Type

data Tele a

type Telescope

mapAbsNamesM

mapAbsNames

replaceEmptyName

data Sort

data Level

data PlusLevel

data LevelAtom

data MetaId

data Blocked t

Definitions

data Clause

clausePats

data ClauseBodyF a

type ClauseBody

type PatVarName

patVarNameToString

nameToPatVarName

data Pattern

namedVarP

type ConPatternInfo

patternVars

properlyMatching

Absurd Lambda

absurdBody

isAbsurdBody

absurdPatternName

isAbsurdPatternName

Pointers and Sharing

ignoreSharing

ignoreSharingType

shared

sharedType

updateSharedFM

updateSharedM

updateShared

pointerChain

compressPointerChain

Smart constructors

var

dontCare

typeDontCare

topSort

set0

set

prop

sort

varSort

sSuc

levelSuc

mkType

impossibleTerm

sgTel

Handling blocked terms.

blockingMeta

blocked

notBlocked

ignoreBlocking

Simple operations on terms and types.

stripDontCare

arity

argName

class Suggest a b

Eliminations.

unSpine

hasElims

argFromElim

isApplyElim

allApplyElims

splitApplyElims

class IsProjElim e

dropProjElims

argsFromElims

Show instances.

Sized instances.

KillRange instances.

UniverseBi instances.