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

type RecordAssignment

type RecordAssignments

type FieldAssignment

data FieldAssignment' a

nameFieldA

exprFieldA

data ModuleAssignment

data BoundName

mkBoundName_

mkBoundName

type Telescope

countTelVars

Declarations

data Declaration

data ModuleApplication

type TypeSignature

type TypeSignatureOrInstanceBlock

type ImportDirective

type Using

type ImportedName

type Renaming

data AsName

data OpenShortHand

type RewriteEqn

type WithExpr

data LHS

data Pattern

data LHSCore

type RHS

data RHS' e

type WhereClause

data WhereClause' decls

data ExprWhere

data Pragma

type Module

data ThingWithFixity x

topLevelModuleName

spanAllowedBeforeModule

Pattern tools

patternNames

patternQNames

Lenses

mapLhsOriginalPattern