Skip to content

doc: fix inaccurate unfold tactic doc #12

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ZRTMRH merged 1 commit into from
Apr 18, 2026
Merged

doc: fix inaccurate unfold tactic doc #12

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Game/Levels/LinearIndependenceSpanWorld/Level03.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ Statement span_mono {A B : Set V} (hAB : A ⊆ B) : span K V A ⊆ span K V B :=
Hint (hidden := true) "Try `intro x hxA`"
intro x hxA
Hint "Now we have `x ∈ span K V A` and need to show `x ∈ span K V B`."
Hint "Let's unfold the definition of span to see what it means for x to be in the span of A."
Hint "Let's unfold the definition of span everywhere to see what it means for x to be in the span of A."
Hint (hidden := true) "Try `unfold span at *`"
unfold span at *
Hint "The span consists of all linear combinations. Let's unfold that definition too."
Expand Down
4 changes: 3 additions & 1 deletion Game/Levels/TutorialWorld/Level05.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,11 @@ Title "The `unfold` and `apply` tactics"
## Summary

If we have some object or function with some definition, `unfold object` will rewrite the object
with its definition everywhere. Lean often unfolds terms automatically, but some tactics and definitions
with its definition in the goal. Lean often unfolds terms automatically, but some tactics and definitions
are not unfolded automatically. The `unfold` tactic also helps make it easier to take the next steps.

`unfold object at h` unfolds at the assumption `h` whereas `unfold object at *` unfolds everywhere.

## Example:

If you have a goal `(P → Q) → (¬ Q → ¬ P)`, with `¬ P` (\"Not\" P) being defined as `P → False`,
Expand Down
Loading