[Agda] Totality checking in Agda

[Henning Basold]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

On 23/01/2019 12:45, Nils Anders Danielsson wrote:
> On 23/01/2019 12.18, Henning Basold wrote:
>> The Foetus productivity checker that is described here: 
>> https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Ter
min
>>
>> 
ationChecker and in the there linked publication by Andreas Abel.
> 
> Agda has for a long time supported more than Foetus: Andreas Abel
> added support for some kind of size-change termination.
> 

But you don't refer to sized types, do you? I remember seeing
something more elaborate than Foetus, but I don't remember any more
where. Do you have a link or paper at hand? Thanks!

Henning
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEMnUmuprSDishxVMiatBsEc2xMm4FAlxIXXMACgkQatBsEc2x
Mm653RAAmgs6SKJz4CRlUDC5CSq+8vPO9AuajehyxJPiRyb39nH2dtaeB3jV9GUs
O5Z7FKL4hGSktXGpQSGv7EAFcOn3GBRWUlEqYg77Gg2eWyAdLWZts/JM4OQY5a2z
98vc8sOFO/gdZCVl6cP884gQTQodo/FVWgEM+nbhL7gYU9a8h4Dkm05mhieYQ0Mg
tHzsvrBKuQKuaYh4vsprIKs93gmGmSOFoAAYC2ubmG89di8ewUE5EcigE0B6jz8f
+Zsx9dfZxJ1AekabDoCldkcIhl+eDe/scdX+0IE6wKzjcibM9g05GaFyq8IhPq0M
AN1/3CQPwQ1VutTaEJj+mST1LxEkGrquNoGiz3dSYfS0j0hiNPvmbv468C/v66hb
p8urLPcbq3Ty0cH8F+9X1/XtGX1o9Ox+za/JD1BRdy9FxTEuO8SBgIxGHo5urdbe
p6QO12+vpCuTfBwzi8Kfjr+72SjFHp92/izZz//GrHXcSOSzHPEosc1cDyka9VF+
Gxfjb7SO4TF/yrOycdB69gUj/roZi8gixw7REAgr4pKaqPU6dJwHoPNPk6749u/8
uUfrDsbs/7FiUsEp7D4+bRNtFPBsgOa6Oa0r/JZJyy+m63Vtpy9je/1dRQTYH/KR
JezwyAA475yoIJZrHEFDZB33HxT84TUipWLAd94VuECyUKn9TMw=
=6OPv
-----END PGP SIGNATURE-----