[Agda] On termination checkers

[david.janin at labri.fr]

Indeed, thank you. I see Andreas point in keeping a small kernel.
And as I am incapable of even touching any termination checker algorithm without breaking it, I won’t complain.

But I still see no way to « encode » inductive list into sized inductive list (with increasing size for cons) in such a way that both append and select have a sized version AND their usual properties are satisfied… A property we could expect from sized type : to be applicable to inductive definitions and derived functions AS IF if there was no termination checker at all but the one induced by sized type argument.

The error I got with the enclosed code when trying refl as final argument is:

  ∞ != j of type Size
  when checking that the expression refl has type
  consN x l ≡ consN x l

in the three cases  N = 1, 2 or 3…  that is all proposed sized extensions of inductive lists (despite these extensions may sound useless and artificial indeed).

By the way, the message above sounds more like a bug than anything else doesn’t it ?


> Le 12 juin 2019 à 13:25, Matthew Daggitt <matthewdaggitt at gmail.com> a écrit :
> 
> Hi David,
>  I asked a very similar question in a recent issue on the Agda Github. You might be interested in Andreas's reply.
> Best,
> Matthew
> 
> On Wed, Jun 12, 2019 at 7:03 PM Andrew Pitts <andrew.pitts at cl.cam.ac.uk> wrote: