Agda.Syntax.Internal

type Args

type NamedArgs

data ConHead

class LensConName a

data Term

type ConInfo

data Elim' a

type Elim

type Elims

type ArgName

argNameToString

stringToArgName

appendArgNames

nameToArgName

data Abs a

data Type' a

type Type

class LensSort a

data Tele a

type Telescope

data Sort

data Level

data PlusLevel

data LevelAtom

Blocked Terms

data NotBlocked

data Blocked t

type Blocked_

stuckOn

Definitions

data Clause

clausePats

type PatVarName

patVarNameToString

nameToPatVarName

data Pattern' x

type Pattern

varP

data DBPatVar

type DeBruijnPattern

namedVarP

namedDBVarP

data ConPatternInfo

noConPatternInfo

toConPatternInfo

fromConPatternInfo

class PatternVars a b

properlyMatching

Explicit substitutions

data Substitution' a

type Substitution

type PatternSubstitution

Views

data EqualityView

isEqualityType

Absurd Lambda

absurdBody

isAbsurdBody

absurdPatternName

isAbsurdPatternName

Pointers and Sharing

ignoreSharing

ignoreSharingType

shared_

updateSharedFM

updateSharedM

updateShared

pointerChain

compressPointerChain

Smart constructors

var

dontCare

typeDontCare

topSort

sort

varSort

sSuc

levelSuc

mkType

isSort

impossibleTerm

hackReifyToMeta

isHackReifyToMeta

Telescopes.

mapAbsNamesM

mapAbsNames

replaceEmptyName

type ListTel' a

type ListTel

telFromList'

telFromList

telToList

class TelToArgs a

class SgTel a

Handling blocked terms.

blockingMeta

blocked

notBlocked

Simple operations on terms and types.

stripDontCare

arity

notInScopeName

class Suggest a b

Eliminations.

unSpine

unSpine'

hasElims

argFromElim

isApplyElim

allApplyElims

splitApplyElims

class IsProjElim e

dropProjElims

argsFromElims

allProjElims

Null instances.

Show instances.

Sized instances and TermSize.

class TermSize a

KillRange instances.

UniverseBi instances.

Simple pretty printing

pDom

NFData instances

data MetaId