Pragmas

Pragmas are comments that are not ignored by Agda but have some special meaning. The general format is:

{-# <PRAGMA_NAME> <arguments> #-}

Index of pragmas

See also Command-line and pragma options.

The INLINE and NOINLINE pragmas

A definition marked with an INLINE pragma is inlined during compilation. If it is a simple definition that does no pattern matching, it is also inlined in function bodies at type-checking time.

Definitions are automatically marked INLINE if they satisfy the following criteria:

  • No pattern matching.
  • Uses each argument at most once.
  • Does not use all its arguments.

Automatic inlining can be prevented using the NOINLINE pragma.

Example:

-- Would be auto-inlined since it doesn't use the type arguments.
_∘_ : {A B C : Set}  (B  C)  (A  B)  A  C
(f ∘ g) x = f (g x)

{-# NOINLINE _∘_ #-} -- prevents auto-inlining

-- Would not be auto-inlined since it's using all its arguments
_o_ : (Set  Set)  (Set  Set)  Set  Set
(F o G) X = F (G X)

{-# INLINE _o_ #-} -- force inlining

The WARNING_ON_USAGE pragma

A library author can use a WARNING_ON_USAGE pragma to attach to a defined name a warning to be raised whenever this name is used.

This would typically be used to declare a name ‘DEPRECATED’ and advise the end-user to port their code before the feature is dropped.

Example:

-- The new name for the identity
id : {A : Set}  A  A
id x = x

-- The deprecated name
λx→x = id

-- The warning
{-# WARNING_ON_USAGE λx→x "DEPRECATED: Use `id` instead of `λx→x`" #-}