Skip to content

doc: update Grove, add table for order API adoption in numeric types - #15120

Open
TwoFX wants to merge 6 commits into
masterfrom
julia/grove-order-0
Open

TwoFX wants to merge 6 commits into
masterfrom
julia/grove-order-0

Conversation

@TwoFX

@TwoFX TwoFX commented Sep 11, 2026

Copy link
Copy Markdown
Member

This PR updates Grove to the latest version and adds a table for order API coverage for numeric types.

@TwoFX TwoFX changed the title doc: update Grove, add table for order API adoption in numeric types - #15097 doc: update Grove, add table for order API adoption in numeric types Sep 11, 2026
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 11, 2026
@TwoFX TwoFX added the grove The standard library changes in this PR should be analyzed using Grove. label Sep 11, 2026
@github-actions

Copy link
Copy Markdown
Contributor

Grove for revision ae43e81.

Grove: upstream invalidated facts not available

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

grove The standard library changes in this PR should be analyzed using Grove. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant