max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: unfold tactic docstring (#5109)

Browse source
This commit is contained in:
Joachim Breitner 2024-08-22 15:58:42 +02:00 • committed by GitHub
parent d975e4302e
commit 01ec8c5e14
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Tactics.lean
View file

@ -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