[Agda] termination proofs

[Nils Anders Danielsson]

On 2012-09-24 13:36, Serge D. Mechveliani wrote:
> Where it is specified in the Language which functions are considered
> as provably terminating?

A conservative approximation of the criterion used in Agda is described
in Section 2.5 of "Subtyping, Declaratively"
(http://www.cse.chalmers.se/~nad/publications/danielsson-altenkirch-subtyping.html).

> Now: how to make a  termination	proof  as explicit as possible?

You can represent termination proofs explicitly in many different ways.
I believe that the paper "Partiality and Recursion in Interactive
Theorem Provers — An Overview" by Bove, Krauss and Sozeau
(http://mattam.org/research/publications/drafts/Partiality_and_Recursion_in_Interactive_Theorem_Provers_-_An_Overview.pdf)
lists some of them.

-- 
/NAD