Skip to content

refactor: name the contract precondition clause requires - #14589

Merged
sgraf812 merged 1 commit into
masterfrom
sg/contract-requires
Jul 30, 2026
Merged

refactor: name the contract precondition clause requires#14589
sgraf812 merged 1 commit into
masterfrom
sg/contract-requires

Conversation

@sgraf812

Copy link
Copy Markdown
Contributor

This PR spells the precondition clause of a def contract requires, pairing with ensures.

The parser declaration Lean.Parser.Command.requireClause is renamed to requiresClause accordingly.

@sgraf812 sgraf812 added the changelog-language Language features and metaprograms label Jul 29, 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 Jul 29, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jul 29, 2026

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b1722adad3d00ad4443a08709b1efb93a78b477c --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-29 12:26:08)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9f011df29fa925487af67848f9b3a2b900dbb17a --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-29 13:37:54)

@leanprover-bot

leanprover-bot commented Jul 29, 2026

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase b1722adad3d00ad4443a08709b1efb93a78b477c --onto a39eab69e1eee9ad38f4efe507907b1026a77808. You can force reference manual CI using the force-manual-ci label. (2026-07-29 12:26:09)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9f011df29fa925487af67848f9b3a2b900dbb17a --onto a39eab69e1eee9ad38f4efe507907b1026a77808. You can force reference manual CI using the force-manual-ci label. (2026-07-29 13:37:55)

The precondition clause of a `def` contract is spelled `requires`, pairing with `ensures`.
@sgraf812
sgraf812 force-pushed the sg/contract-requires branch from 2f5ee7c to 099d02b Compare July 29, 2026 13:16
@sgraf812
sgraf812 marked this pull request as ready for review July 30, 2026 11:37
@sgraf812
sgraf812 enabled auto-merge July 30, 2026 11:37
@sgraf812
sgraf812 added this pull request to the merge queue Jul 30, 2026
Merged via the queue into master with commit 2d0879c Jul 30, 2026
22 checks passed
@sgraf812
sgraf812 deleted the sg/contract-requires branch July 30, 2026 12:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-language Language features and metaprograms 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.

2 participants