[Agda] convenient induction on non-empty list?

[Jason Hu]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210819/7171d44d/attachment.html>