[Agda] Totality checking in Agda

[Marko Dimjašević]

Hi Nils,

On Wed, 2019-01-23 at 08:49 +0100, Nils Anders Danielsson wrote:
> 
> I don't think there is a single text (other than the source code)
> that
> describes everything in detail. What kind of information are you
> looking
> for?


There are several things I am looking for. I am interested in:

1) What form of recursion is allowed in Agda for terminating functions?

2) How does Agda check for productivity?

3) How to write a main program, which should be of type IO (), and if
this is possible at all if partial functions are not allowed in Agda?

4) In Idris, one can annotate a function as partial; I found no way of
writing partial functions in Agda. I read lecture notes from the
International LerNetALFA Summer School 2008 and in particular chapter 2
titled "Dependent Types at Work" that has a section "General Recursion
and Partial Functions", but I still don't see how to write partial
functions in Agda; what is given there and in the Agda wiki doesn't
look to me like partial functions, but total functions instead because
those examples are defined on their whole domain.

5) How to write productive programs in Agda that use fuel to ensure
their totality?


-- 
Regards,
Marko Dimjašević <marko at dimjasevic.net>
https://dimjasevic.net/marko
PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA
Learn email self-defense! https://emailselfdefense.fsf.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190123/666a47be/attachment.sig>