Switching off termination checker [Re: [Agda] simple example]
Andreas Abel
andreas.abel at ifi.lmu.de
Fri Aug 17 09:21:31 CEST 2012
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 #-}
Cheers
Andreas
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list