Agda.Syntax.Concrete

Expressions

data Expr

data OpApp e

fromOrdinary

appView

data AppView

Bindings

type LamBinding

data LamBinding' a

type TypedBindings

data TypedBindings' a

type TypedBinding

data TypedBinding' e

data ColoredTypedBinding

data BoundName

mkBoundName_

mkBoundName

type Telescope

countTelVars

Declarations

data Declaration

data ModuleApplication

type TypeSignature

type TypeSignatureOrInstanceBlock

type Constructor

data ImportDirective

data UsingOrHiding

data ImportedName

data Renaming

data AsName

defaultImportDir

data OpenShortHand

type RewriteEqn

type WithExpr

data LHS

data Pattern

data LHSCore

type RHS

data RHS' e

type WhereClause

data WhereClause' decls

data Pragma

type Module

data ThingWithFixity x

topLevelModuleName

Pattern tools

patternNames

patternQNames

Lenses

mapLhsOriginalPattern

Concrete instances

type Color

type Arg a

type NamedArg a

type ArgInfo