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