[Agda] simple example

[Serge D. Mechveliani]

On Thu, Aug 16, 2012 at 01:39:25PM +0200, Dan Ros?n wrote:
> >
> > 1. Is it possible to  postulate termination  for a given function?
> >
> 
> Yes. From the release notes in doc/release-notes/2-3-2.txt:
> 
> * New: Pragma NO_TERMINATION_CHECK to switch off termination checker
>   for individual function definitions and mutual blocks.
> 
>   The pragma must precede a function definition or a mutual block.
>   Examples (see test/succeed/NoTerminationCheck.agda):
> 
>   1. Skipping a single definition: before type signature.
> 
>        {-# NO_TERMINATION_CHECK #-}
>        a : A
>        a = a
> [..]


I have  Agda-2.3.0.1.
Is  NO_TERMINATION_CHECK  in a non-official release?

Regards,

------
Sergei