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¶
- BUILTIN
- CATCHALL
- COMPILE
- FOREIGN
- NO_POSITIVITY_CHECK
- NO_TERMINATION_CHECK
- NON_TERMINATING
- POLARITY
- STATIC
- TERMINATING
- INLINE
- NOINLINE
- WARNING_ON_USAGE
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`" #-}