[Agda] Agda "trusted core".

[Pierre Hyvernat]

> > > Another related question is whether we want to allow
> > > non-terminating definitions.
> > >
> > 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
> 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.
>
As a matter of fact, I also agree with that. We do want to write program
that do not pass termination check...

This is also for this very same reason that I agree with Peter about
introducing a "trusted" core which guarantees termination.
(Non inductive function, and possibly structurally inductive
definitions...)


This is also why I would like to see a coinductive mechanism: I have
experimented with writing "coinductive" types using the fact that no
termination check is performed at type checking; but this doesn't work
well.  I managed to send the type checker into infinite loops (which is
not supposed to happen)...


Pierre
--