Skip to content

Fix misleading comment in tactics2, add and_map exercise - #2

Merged
SamuelSchlesinger merged 1 commit into
mainfrom
fix/tactics2-apply-comment
Apr 2, 2026
Merged

Fix misleading comment in tactics2, add and_map exercise#2
SamuelSchlesinger merged 1 commit into
mainfrom
fix/tactics2-apply-comment

Conversation

@SamuelSchlesinger

Copy link
Copy Markdown
Owner

Summary

  • Fix the misleading "Combine constructor and apply" comment on and_swap (which doesn't need apply) — now reads "Use constructor and the .left/.right accessors together"
  • Add a new and_map exercise that genuinely requires both constructor and apply

Closes #1

Test plan

  • Exercise file builds (only sorry warnings)
  • Solution file builds cleanly

The and_swap comment said "Combine constructor and apply" but apply
wasn't needed. Reword that comment and add and_map, which genuinely
requires both tactics.

Closes #1
@SamuelSchlesinger
SamuelSchlesinger merged commit 0f0e4c8 into main Apr 2, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Confusing instruction in 10_tactics/tactics2.lean

1 participant