Termination Checking

Note

This is a stub.

With-functions

Pragmas and Options

  • The NON_TERMINATING pragma

    This is a safer version of TERMINATING which doesn’t treat the affected functions as terminating. This means that NON_TERMINATING functions do not reduce during type checking. They do reduce at run-time and when invoking C-c C-n at top-level (but not in a hole). The pragma was added in Agda 2.4.2.

  • The TERMINATING pragma

    Switches off termination checker for individual function definitions and mutual blocks and marks them as terminating. Since Agda 2.4.2.1 replaced the NO_TERMINATION_CHECK pragma.

    The pragma must precede a function definition or a mutual block. The pragma cannot be used in --safe mode.

    Examples:

    • Skipping a single definition: before type signature:

      {-# TERMINATING #-}
      a : A
      a = a
      
    • Skipping a single definition: before first clause:

      b : A
      {-# TERMINATING #-}
      b = b
      
    • Skipping an old-style mutual block: Before mutual keyword:

      {-# TERMINATING #-}
      mutual
        c : A
        c = d
      
        d : A
        d = c
      
    • Skipping an old-style mutual block: Somewhere within mutual block before a type signature or first function clause:

      mutual
       {-# TERMINATING #-}
       e : A
       e = f
      
       f : A
       f = e
      
    • Skipping a new-style mutual block: Anywhere before a type signature or first function clause in the block:

      g : A
      h : A
      
      g = h
      {-# TERMINATING #-}
      h = g