Skip to content

feat: basic documentation for grindHom and grindHomPred#904

Merged
robsimmons merged 1 commit into
nightly-testingfrom
bump-2026-07-24
Jul 24, 2026
Merged

feat: basic documentation for grindHom and grindHomPred#904
robsimmons merged 1 commit into
nightly-testingfrom
bump-2026-07-24

Conversation

@robsimmons

Copy link
Copy Markdown
Collaborator

Short explanation based on the existing docs, and a note that this could use an example in the future.

@robsimmons robsimmons changed the title basic documentation for grindHom and grindHomPred feat: basic documentation for grindHom and grindHomPred Jul 24, 2026
@leanprover-bot leanprover-bot added the HTML available HTML has been generated for this PR label Jul 24, 2026
@github-actions

Copy link
Copy Markdown
Contributor

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

@robsimmons
robsimmons merged commit f4e1f56 into nightly-testing Jul 24, 2026
10 of 11 checks passed
@robsimmons
robsimmons deleted the bump-2026-07-24 branch July 24, 2026 18:08
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