Switching off termination checker [Re: [Agda] simple example]

[Serge D. Mechveliani]

On Fri, Aug 17, 2012 at 09:21:31AM +0200, Andreas Abel wrote:
> Hello Serge,
>
> On 16.08.12 7:13 PM, Serge D. Mechveliani wrote:
>> I have  Agda-2.3.0.1.
>> Is  NO_TERMINATION_CHECK  in a non-official release?
>
> It is in the development version of Agda (darcs repository).
>
> In Agda-2.3.0 and before you can only turn off termination checking for  
> a whole file via
>
>   {-# OPTIONS --no-termination-check #-}
>

I see. Thanks to people.
I think, it is usable in practice, and the new-coming pragma is even 
more usable.

Sergei.