From ffaadcc990ca91c705b21d248cb7649770669d28 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 23 Oct 2025 22:54:40 +0200 Subject: [PATCH] doc: warning for wf_preprocess (#10897) This PR adds a warning to `wf_preproces` that these lemmas can be used to introduce hidden partiality. --------- Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> --- src/Init/Tactics.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 007ad07e8b..a652186103 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -2317,6 +2317,12 @@ Theorems tagged with the `wf_preprocess` attribute are used during the processin by well-founded recursion. They are applied to the function's body to add additional hypotheses, such as replacing `if c then _ else _` with `if h : c then _ else _` or `xs.map` with `xs.attach.map`. Also see `wfParam`. + +Warning: These rewrites are only applied to the declaration for the purpose of the logical +definition, but do not affect the compiled code. In particular they can cause a function definition +that diverges as compiled to be accepted without an explicit `partial` keyword, for example if they +remove irrelevant subterms or change the evaluation order by hiding terms under binders. Therefore +avoid tagging theorems with `[wf_preprocess]` unless they preserve also operational behavior. -/ syntax (name := wf_preprocess) "wf_preprocess" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr