Agda.Syntax.Concrete.Definitions

IsAbstract argument: We record whether a declaration was made in an abstract block.

ArgInfo argument: Axioms and functions can be declared irrelevant. (Hiding should be NotHidden.)

An uncategorized function clause, could be a function clause without type signature or a pattern lhs (e.g. for irrefutable let). The Declaration is the actual FunClause.

Block of function clauses (we have seen the type signature before). The Declarations are the original declarations that were processed into this FunDef and are only used in notSoNiceDeclaration. Andreas, 2017-01-01: Because of issue #2372, we add IsInstance here. An alias should know that it is an instance.

(Maybe Range) gives range of the pattern declaration.

Empty abstract block.

Empty data _ where block.

Empty field block.

Empty variable block.

Empty instance block

Empty macro block.

Empty mutual block.

Empty postulate block.

Empty private block.

Empty primitive block.

A Hidden identifier in a variable declaration. Hiding has no effect there as generalized variables are always hidden (or instance variables).

A {-# CATCHALL #-} pragma that does not precede a function clause.

Invalid definition in a constructor block

Invalid constructor block (not inside an interleaved mutual block)

A {-# NON_COVERING #-} pragma that does not apply to any function.

A {-# NO_POSITIVITY_CHECK #-} pragma that does not apply to any data or record type.

A {-# NO_UNIVERSE_CHECK #-} pragma that does not apply to a data or record type.

A {-# TERMINATING #-} and {-# NON_TERMINATING #-} pragma that does not apply to any function.

Definitions (e.g. constructors or functions) without a declaration.

Declarations (e.g. type signatures) without a definition.

private has no effect on open public. (But the user might think so.) KwRange is the range of the public keyword.

abstract has no effect on open public. (But the user might think so.) KwRange is the range of the public keyword.

Pragma {-# NO_TERMINATION_CHECK #-} has been replaced by {-# TERMINATING #-} and {-# NON_TERMINATING #-}.

COMPILE pragmas are not allowed in safe mode.

ETA pragma is unsafe.

INJECTIVE pragma is unsafe.

NON_COVERING pragma is unsafe.

NO_POSITIVITY_CHECK pragma is unsafe.

NO_UNIVERSE_CHECK pragma is unsafe.

NON_TERMINATING pragma is unsafe.

POLARITY pragma is unsafe.

TERMINATING pragma is unsafe.

abstract block with nothing that can (newly) be made abstract.

instance block with nothing that can (newly) become an instance.

macro block with nothing that can (newly) be made macro.

private block with nothing that can (newly) be made private.