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

Serge D. Mechveliani mechvel at botik.ru
Fri Aug 17 11:01:55 CEST 2012

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-
>> 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.


More information about the Agda mailing list