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