Agda.Syntax.Abstract

type Color

type Arg a

type Dom a

type NamedArg a

type ArgInfo

type Args

data Expr

type Assign

type Assigns

data Axiom

type Ren a

data Declaration

class GetDefInfo a

data ModuleApplication

data Pragma

data LetBinding

type TypeSignature

type Constructor

type Field

data LamBinding

data TypedBindings

data TypedBinding

type Telescope

data Clause' lhs

type Clause

type SpineClause

data RHS

data SpineLHS

data LHS

data LHSCore' e

type LHSCore

class LHSToSpine a b

lhsCoreToSpine

spineToLhsCore

lhsCoreApp

lhsCoreAddSpine

lhsCoreAllPatterns

lhsCoreToPattern

mapLHSHead

Patterns

data Pattern' e

type Pattern

type Patterns

class IsProjP a

class AllNames a

axiomName

class AnyAbstract a

app

patternToExpr

type PatternSynDefn

type PatternSynDefns

lambdaLiftExpr

substPattern

class SubstExpr a

insertImplicitPatSynArgs