Joachim Breitner 4016a80f66

feat: nested well-founded recursion via automatic preprocessing (#6744) ...

This PR extend the preprocessing of well-founded recursive definitions
to bring assumptions like `h✝ : x ∈ xs` into scope automatically.

This fixes #5471, and follows (roughly) the design written there.
See the module docs at `src/Lean/Elab/PreDefinition/WF/AutoAttach.lean`
for details on the implementation.

This only works for higher-order functions that have a suitable setup.
See for example section “Well-founded recursion preprocessing setup” in
`src/Init/Data/List/Attach.lean`.

This does not change the `decreasing_tactic`, so in some cases there is
still the need for a manual termination proof some cases. We expect a
better termination tactic in the near future.

2025-02-10 16:43:41 +00:00

0 lines

Text

Raw Blame History