[Agda] convenient induction on non-empty list?

[Matthew Daggitt]

That is weird. I don't have any concrete suggestions apart from the one
you've already mentioned, apologies, but I'd definitely advise filing a bug
report on the Agda repo.

On Fri, Aug 20, 2021 at 6:45 AM Jason Hu <fdhzs2010 at hotmail.com> wrote:

> Hi all,
>
>
>
> It sounds like a stupid question but it seems to me there isn’t a
> convenient way to do it. What I want to do is to do induction on a
> non-empty list as defined in the stdlib in a “standard” way. To illustrate
> the problem, consider the following program:
>
>
>
> open import Data.Nat
>
> open import Data.List
>
> open import Data.List.NonEmpty
>
>
>
> len : List⁺ ℕ → ℕ
>
> len (x ∷ []) = 1
>
> len (x ∷ y ∷ l) = len (y ∷ l)
>
>
>
> As of 2.6.2, Agda doesn’t like this definition and complains that len does
> not terminate. What I am looking for is a solution that does not require
> defining a “helper” which handle the underlying list, and the “main”
> function which does the job separately.
>
>
>
> Any idea is appreciated.
>
>
>
> Thanks,
>
> Jason Hu
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210820/c28bcdb5/attachment.html>