Pragmas

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

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

Index of pragmas

See also Command-line and pragma options.

The DISPLAY pragma

Users can declare a DISPLAY pragma:

  1. {-# DISPLAY f e1 .. en = e #-}

This causes f e1 .. en to be printed in the same way as e, where ei can bind variables used in e. The expressions ei and e are scope checked, but not type checked.

For example this can be used to print overloaded (instance) functions with the overloaded name:

  1. instance
  2.   NumNat : Num Nat
  3.   NumNat = record { ..; _+_ = natPlus }
  5. {-# DISPLAY natPlus a b = a + b #-}

Limitations

  • Left-hand sides are restricted to variables, constructors, defined functions or types, and literals. In particular, lambdas are not allowed in left-hand sides.

  • Since DISPLAY pragmas are not type checked implicit argument insertion may not work properly if the type of f computes to an implicit function space after pattern matching.

The INJECTIVE pragma

Injective pragmas can be used to mark a definition as injective for the pattern matching unifier. This can be used as a version of --injective-type-constructors that only applies to specific datatypes.

Example:

  1. open import Agda.Builtin.Equality
  2. open import Agda.Builtin.Nat
  4. data Fin : Nat → Set where
  5.   zero : {n : Nat} → Fin (suc n)
  6.   suc  : {n : Nat} → Fin n → Fin (suc n)
  8. {-# INJECTIVE Fin #-}
  10. Fin-injective : {m n : Nat} → Fin m ≡ Fin n → m ≡ n
  11. Fin-injective refl = refl

Aside from datatypes, this pragma can also be used to mark other definitions as being injective (for example postulates).

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.

When the --auto-inline command-line option is enabled, 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:

  1. -- Would be auto-inlined since it doesn't use the type arguments.
  2. _∘_ : {A B C : Set} → (B → C) → (A → B) → A → C
  3. (f ∘ g) x = f (g x)
  5. {-# NOINLINE _∘_ #-} -- prevents auto-inlining
  7. -- Would not be auto-inlined since it's using all its arguments
  8. _o_ : (Set → Set) → (Set → Set) → Set → Set
  9. (F o G) X = F (G X)
  11. {-# INLINE _o_ #-} -- force inlining

The NON_COVERING pragma

New in version 2.6.1.

The NON_COVERING pragma can be placed before a function (or a block of mutually defined functions) which the user knows to be partial. To be used as a version of --allow-incomplete-matches that only applies to specific functions.

The NOT_PROJECTION_LIKE pragma

New in version 2.6.3.

The NOT_PROJECTION_LIKE pragma disables projection-likeness analysis for a particular function, which must be defined before it can be affected by the pragma. To be used as a version of --no-projection-like that only applies to specific functions.

For example, suppose you have a function which projects a field from an instance argument, and instance selection depends on a visible argument. If an application of this function is generated by metaprogramming, and inserted in the source code by elaborate-and-give (C-c C-m in Emacs), the visible argument would instead be printed as _, because it was erased!

Example:

  1. open import Agda.Builtin.Bool
  3. record P (n : Nat) : Set where
  4.   field the-bool : Bool
  5. open P
  7. -- Agda would normally mark this projection-like, so it would have its
  8. -- (n : Nat) argument erased when printing, including by e.g.
  9. -- elaborate-and-give
  10. get-bool-from-p : (n : Nat) ⦃ has-p : P n ⦄ → Bool
  11. get-bool-from-p _ ⦃ p ⦄ = p .the-bool
  12. {-# NOT_PROJECTION_LIKE get-bool-from-p #-}
  14. -- With the pragma, it gets treated as a regular function.

The OPTIONS pragma

Some options can be given at the top of .agda files in the form

{-# OPTIONS --{opt₁} --{opt₂} ... #-}

The possible options are listed in Command-line and pragma options.

The WARNING_ON_ pragmas

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 (since Agda 2.5.4).

Similarly they can use a WARNING_ON_IMPORT pragma to attach to a module a warning to be raised whenever this module is imported (since Agda 2.6.1).

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

Users can turn these warnings off by using the --warn=noUserWarning option. For more information about the warning machinery, see Warnings.

Example:

  1. -- The new name for the identity
  2. id : {A : Set} → A → A
  3. id x = x
  5. -- The deprecated name
  6. λx→x = id
  8. -- The warning
  9. {-# WARNING_ON_USAGE λx→x "DEPRECATED: Use `id` instead of `λx→x`" #-}
  10. {-# WARNING_ON_IMPORT "DEPRECATED: Use module `Function.Identity` rather than `Identity`" #-}