Module abs 

Abstract terms and declarations.

Modules

ast 🔒

Abstract terms.

decl 🔒

Declarations.

decl_impl 🔒

Declarations’ trivial trait implementations.

desugar

Surface to abstract, scope-checking.

pretty 🔒

Structs

AbsClause

Clause information in abstract syntax. Agda.

AbsCodataInfo

AbsConsInfo

AbsDataInfo

AbsDefnInfo

AbsProjInfo

AppView

Application’s internal view. Agda.

Enums

Abs

The abstract syntax.

AbsDecl

Declaration. Agda.

Type Aliases

AbsCopat

Patterns in the abstract syntax.

AbsPat

AbsTele

Telescopes in the abstract syntax.

Bind

Name binding.