Agda.Syntax.Internal

data Term

type Args

data Elim

data Abs a

data Type

data Tele a

type Telescope

data Sort

data Level

data PlusLevel

data LevelAtom

data MetaId

data Blocked t

# Definitions

data Clause

data ClauseBody

data Pattern

patternVars

properlyMatching

# Smart constructors

ignoreSharing

ignoreSharingType

shared

sharedType

updateSharedFM

updateSharedM

updateShared

pointerChain

compressPointerChain

var

typeDontCare

topSort

set0

set

prop

sort

varSort

sSuc

levelSuc

mkType

impossibleTerm

# Handling blocked terms.

blockingMeta

blocked

notBlocked

ignoreBlocking

# Simple operations on terms and types.

stripDontCare

arity

argName

# Show instances.

# Sized instances.

# KillRange instances.

# UniverseBi instances.