[Agda] Agda "trusted core".

[csetzer]

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


-- 
-----------------------------------------------------------------------------
Anton Setzer                            Telephone:
Department of Computer Science          (national)        (01792) 513368
University of Wales Swansea             (international) +44 1792  513368
Singleton Park                          Fax:
Swansea SA2 8PP                         (national)        (01792) 295708
UK                                      (international) +44 1792  295708

Visiting address:                       Email: a.g.setzer at swan.ac.uk
Faraday Building,                       WWW:
Computer Science Dept.            http://www.cs.swan.ac.uk/~csetzer/
2nd floor, room 211. 
------------------------------------------------------------------------------