[Agda] Agda "trusted core".

[Bengt Nordström]

I agree completely with Anton, and this has always been the main reason 
for having it. But I also think it should be made clear whether a 
program has been checked for termination.

Bengt

csetzer wrote:
> Pierre Hyvernat wrote:
> 
>>
>> Another related question is whether we want to allow non-terminating
>> definitions. Right now, you can write anything; but it needs not pass
>> termination check?
>> Is it a Good thing or a Bad thing?
>>
>>
> 
> It is a good thing, and for me it is essential. Otherwise it  wouldn't 
> be possible  to experiment with definitions which go beyond Agda, e.g. 
> the Mahlo universe, the closed formulisation of inductive recursive 
> definitions or interactive programs formulated directly in Agda.
> Since Agda with termination check can't be turing complete, there will
> always be extensions which don't pass the termination checker but
> are  perfectly okay.
> 
>>
>> Pierre Hyvernat
> 
> 
>