Why termination checked works with List.map?

Stream: new members

[Jakub Nowak]

I though I would have to use List.attach to make it work, but apparently termination checker already knows that with List.map arguments belong to the list. Where did termination checker got this from?

inductive Tree where
| leaf (n : Nat)
| node (children : List Tree)

def Tree.sum : Tree → Nat
| .leaf n => n
| .node children => children.map sum |>.sum
termination_by t => t
decreasing_by
  rename_i t h
  guard_hyp h : t ∈ children

[Henrik Böving]

There is a new mechanism called wf_preprocess that is basically able to heuristically insert List.attach and similar functions on the fly

[Jakub Nowak]

Can you point me where in code is this defined? I want to know how to implement wf_preprocess for my own types.

[Jakub Nowak]

nvm, I've found it
https://github.com/leanprover/lean4/blob/f317e28d842bad09a6111e1f72dda8a2c0bdc3c5/src/Init/Data/List/Attach.lean#L810-L817

[Jakub Nowak]

Cool feature!