Agda.Syntax.Concrete

# Expressions

data Expr
appView
data AppView

# Bindings

data LamBinding
data TypedBindings
data TypedBinding
data BoundName
mkBoundName_
type Telescope

# Declarations

data Declaration
type TypeSignature
type Constructor
type Field
data ImportDirective
data UsingOrHiding
data ImportedName
data Renaming
data AsName
defaultImportDir
data OpenShortHand
data LHS
data Pattern
data RHS
data WhereClause
data Pragma
type Module
topLevelModuleName