> > > I have Agda-2.3.0.1. > Is NO_TERMINATION_CHECK in a non-official release? > It is in the development version which you can get via darcs, see information under "Development version" at http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Download /Dan