; Iter it.2 positive: structural list length. `len` recurses on the
; Cons-tail `t` (a constructor sub-component of `xs`) via a plain,
; non-tail `(app len t)`. Structurally guarded at position 0, pure,
; total, Diverge-free. No `tail-app` marker — this is the structural
; recursion form the it.2 guardedness check must accept on its own.

(module struct_rec_list_len

  (data IntList
    (ctor INil)
    (ctor ICons (con Int) (con IntList)))

  (fn len
    (doc "Length of an IntList via structural recursion on the tail.")
    (type
      (fn-type
        (params (con IntList))
        (ret (con Int))))
    (params xs)
    (body
      (match xs
        (case (pat-ctor INil) 0)
        (case (pat-ctor ICons h t)
          (app + 1 (app len t)))))))