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