[Agda] Agda "trusted core".

Peter G. Hancock hancock at spamcop.net
Thu Dec 9 13:06:20 CET 2004


I hope this is a suitable way to float an idea:

I have felt it would be a good idea to delimit the scopes in which
recursion is to be allowed with an explicit "rec/mutual" keyword.  There
is something extremely dangerous about recursion, and ideally there
should be just a few instances of recursive definitions in an Agda
program.  The recursion-free fragment of Agda would be a kind of 
trusted core. 

[In the editor, ideally sirens should go off and red lights flash when
one enters the scope of a ret.]

Peter Hancock

More information about the Agda mailing list