[Agda] Declaration-wise termination checking.
Andreas Abel
andreas.abel at ifi.lmu.de
Thu Mar 8 19:43:53 CET 2012
Tada! Finally, the long standing feature request (issue 16) has been
implemented. Now you can
{-# NO_TERMINATION_CHECK #-}
individual definitions and mutual blocks.
See test/succeed/NoTerminationCheck.agda for example use. Enjoy,
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