Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: add Int16/Int32/Int64 #5885

Merged
merged 11 commits into from
Nov 4, 2024
Merged

feat: add Int16/Int32/Int64 #5885

merged 11 commits into from
Nov 4, 2024

Conversation

hargoniX
Copy link
Contributor

This adds all fixed width integers with the exception of ssize_t so the code is quick to review as everything just behaves the same.

@hargoniX hargoniX requested a review from kim-em as a code owner October 30, 2024 08:48
@hargoniX hargoniX added the release-ci Enable all CI checks for a PR, like is done for releases label Oct 30, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 30, 2024 09:11 Inactive
@hargoniX hargoniX requested a review from TwoFX October 30, 2024 09:15
@hargoniX hargoniX changed the title feat: add Int8/Int16/Int32/Int64 feat: add Int16/Int32/Int64 Oct 30, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 30, 2024 14:29 Inactive
@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 Oct 30, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 30, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5885
67ec1f6
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 30, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5885
2adcae2
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Oct 30, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 30, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ✅ Mathlib branch lean-pr-testing-5885 has successfully built against this PR. (2024-10-30 16:18:28) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4af93813f24d2a758f7acca492186f53dbb24980 --onto 0fcee100e7ea382069854d91e854265c56b54428. (2024-10-31 14:56:04)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c61ced3f15fad68fbeaf0158c2bc9fe0af5d2e4d --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-04 13:23:37)

TwoFX
TwoFX reviewed Oct 31, 2024
View reviewed changes
src/include/lean/lean.h Outdated Show resolved Hide resolved
src/include/lean/lean.h Outdated Show resolved Hide resolved
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 31, 2024 13:36 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 31, 2024 14:02 Inactive
TwoFX
TwoFX reviewed Oct 31, 2024
View reviewed changes
src/include/lean/lean.h Outdated Show resolved Hide resolved
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc October 31, 2024 17:48 Inactive
TwoFX
TwoFX approved these changes Nov 4, 2024
View reviewed changes
Copy link
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM except for the request for documentation.

src/Init/Data/SInt/Basic.lean Show resolved Hide resolved
@hargoniX hargoniX enabled auto-merge November 4, 2024 12:18
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc November 4, 2024 12:30 Inactive
@hargoniX hargoniX added this pull request to the merge queue Nov 4, 2024
Merged via the queue into master with commit 93dd6f2 Nov 4, 2024
22 checks passed
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this pull request Nov 4, 2024
@hargoniX @JovanGerb
feat: add Int16/Int32/Int64 (leanprover#5885)
7338e86 
This adds all fixed width integers with the exception of `ssize_t` so
the code is quick to review as everything just behaves the same.
@hargoniX hargoniX mentioned this pull request Nov 5, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tobiasgrosser tobiasgrosser tobiasgrosser left review comments

@TwoFX TwoFX TwoFX approved these changes

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@hargoniX @leanprover-community-bot @tobiasgrosser @TwoFX