From 01ec8c5e144d8cb96ec9bf8a3267378a7d03d562 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 22 Aug 2024 15:58:42 +0200 Subject: [PATCH] doc: `unfold` tactic docstring (#5109) --- src/Init/Tactics.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index baf0051511..0f1c715cd0 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -679,9 +679,9 @@ syntax (name := delta) "delta" (ppSpace colGt ident)+ (location)? : tactic * `unfold id` unfolds definition `id`. * `unfold id1 id2 ...` is equivalent to `unfold id1; unfold id2; ...`. -For non-recursive definitions, this tactic is identical to `delta`. -For definitions by pattern matching, it uses "equation lemmas" which are -autogenerated for each match arm. +For non-recursive definitions, this tactic is identical to `delta`. For recursive definitions, +it uses the "unfolding lemma" `id.eq_def`, which is generated for each recursive definition, +to unfold according to the recursive definition given by the user. -/ syntax (name := unfold) "unfold" (ppSpace colGt ident)+ (location)? : tactic