Agda.Syntax.Concrete.Definitions.Types

The nice declarations. No fixity declarations and function definitions are contained in a single constructor instead of spread out between type signatures and clauses. The private, postulate, abstract and instance modifiers have been distributed to the individual declarations.

Observe the order of components:

Range Fixity' Access IsAbstract IsInstance TerminationCheck PositivityCheck

further attributes

(Q)Name

content (Expr, Declaration ...)

Termination measure is, for now, a variable name.

Only Axioms.

Only Axioms.

One clause in a function definition. There is no guarantee that the LHS actually declares the Name. We will have to check that later.

When processing a mutual block we collect the various checks present in the block before combining them.

In an inferred mutual block we keep accumulating nice declarations until all of the lone signatures have an attached definition. The type is therefore a bit span-like: we return an initial segment (the inferred mutual block) together with leftovers.

In an `interleaved mutual' block we collect the data signatures, function signatures, as well as their associated constructors and function clauses respectively. Each signature is given a position in the block (from 0 onwards) and each set of constructor / clauses is given a *distinct* one. This allows for interleaved forward declarations similar to what one gets in a new-style mutual block.

Numbering declarations in an interleaved mutual block.

Several declarations expect only type signatures as sub-declarations. These are:

The kind of the forward declaration.