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