[Agda] Agda "trusted core".

[Peter G. Hancock]

Hello, 

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