Agda.Syntax.Internal
type Args
type NamedArgs
data ConHead
class LensConName a
data Term
data Elim' a
type Elim
type Elims
type ArgName
data Abs a
data Type' a
type Type
class LensSort a
data Tele a
type Telescope
data Sort
data Level
data PlusLevel
data LevelAtom
data NotBlocked
data Blocked t
type Blocked_
data Clause
data ClauseBodyF a
type ClauseBody
type PatVarName
data Pattern' x
type Pattern
type DeBruijnPattern
data ConPatternInfo
data Substitution' a
type Substitution
type PatternSubstitution
data EqualityView
class SgTel a
class Suggest a b
class IsProjElim e
class TermSize a
data MetaId