Agda.Syntax.Internal

data Term

data Type

data Sort

data Blocked t

type Args

data Tele a

type Telescope

data Abs a

telFromList

telToList

data Clauses

originalClause

data Clause

data ClauseBody

data Pattern

data MetaId

arity

argName

# Views

data FunView

funView

# Smart constructors

blockingMeta

blocked

notBlocked

ignoreBlocking

teleLam

getSort

unEl

sSuc

sLub

impossibleTerm