Skip to content

doc: move replace tactic next to have#852

Open
frangio wants to merge 1 commit into
leanprover:mainfrom
frangio:tactic-replace
Open

doc: move replace tactic next to have#852
frangio wants to merge 1 commit into
leanprover:mainfrom
frangio:tactic-replace

Conversation

@frangio

@frangio frangio commented May 23, 2026

Copy link
Copy Markdown

replace is currently in the Rewriting section (rw, etc.), but it seems to belong with have instead.

@david-christiansen david-christiansen added the HTML available HTML has been generated for this PR label May 27, 2026
@github-actions

Copy link
Copy Markdown
Contributor

Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 6143cb6.

@frangio frangio changed the title Move replace tactic next to have doc: move replace tactic next to have May 27, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

HTML available HTML has been generated for this PR

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants