Agda-2.2.6: A dependently typed functional programming language and proof assistant




data NiceDeclaration Source

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, and abstract modifiers have been distributed to the individual declarations.

data Clause Source

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