chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream #3579

kim-em · 2024-03-03T10:56:56Z

No description provided.

leanprover-community-mathlib4-bot · 2024-03-04T03:37:52Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-3579 build failed against this PR. (2024-03-04 03:37:50) View Log
🟡 Mathlib branch lean-pr-testing-3579 build this PR didn't complete normally. (2024-03-04 04:22:38) View Log
💥 Mathlib branch lean-pr-testing-3579 build failed against this PR. (2024-03-04 04:27:22) View Log
🟡 Mathlib branch lean-pr-testing-3579 build this PR didn't complete normally. (2024-03-04 05:13:01) View Log
💥 Mathlib branch lean-pr-testing-3579 build failed against this PR. (2024-03-04 05:23:12) View Log
💥 Mathlib branch lean-pr-testing-3579 build failed against this PR. (2024-03-07 04:30:57) View Log
💥 Mathlib branch lean-pr-testing-3579 build failed against this PR. (2024-03-07 04:41:46) View Log
❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 611b1746896bbadf459c00cc218fa31cf51b4e08 --onto ae492265fec103aa834d897bf9f68c94d10f0785. (2024-03-07 05:05:53)
💥 Mathlib branch lean-pr-testing-3579 build failed against this PR. (2024-03-13 04:22:15) View Log
🟡 Mathlib branch lean-pr-testing-3579 build against this PR was cancelled. (2024-03-13 04:45:56) View Log
💥 Mathlib branch lean-pr-testing-3579 build failed against this PR. (2024-03-13 04:59:40) View Log
💥 Mathlib branch lean-pr-testing-3579 build failed against this PR. (2024-03-13 05:16:53) View Log
💥 Mathlib branch lean-pr-testing-3579 build failed against this PR. (2024-03-13 05:23:52) View Log
🟡 Mathlib branch lean-pr-testing-3579 build against this PR was cancelled. (2024-03-13 05:38:17) View Log
🟡 Mathlib branch lean-pr-testing-3579 build this PR didn't complete normally. (2024-03-13 05:39:14) View Log
💥 Mathlib branch lean-pr-testing-3579 build failed against this PR. (2024-03-13 06:19:01) View Log
🟡 Mathlib branch lean-pr-testing-3579 build this PR didn't complete normally. (2024-03-13 08:13:10) View Log

fix tests fix tests

kim-em mentioned this pull request Mar 3, 2024

feat: add Nat.pred_eq_sub_one #3578

Closed

kim-em added the full-ci label Mar 3, 2024

kim-em force-pushed the simp_succ_eq_add_one branch from e4da674 to 56670a0 Compare March 4, 2024 02:49

github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 4, 2024 03:03 Inactive

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 4, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 4, 2024

Update lean-toolchain for testing leanprover/lean4#3579

1fc6571

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 4, 2024

Update lean-toolchain for testing leanprover/lean4#3579

c099195

leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 4, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 4, 2024

Trigger CI for leanprover/lean4#3579

f495a4a

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 4, 2024

Trigger CI for leanprover/lean4#3579

9ad5f2b

github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 4, 2024 04:30 Inactive

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 4, 2024

Trigger CI for leanprover/lean4#3579

fef6851

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 4, 2024

Trigger CI for leanprover/lean4#3579

03a58a6

github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 7, 2024 04:36 Inactive

kim-em added 3 commits March 13, 2024 14:28

chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream

9a649e6

fix tests fix tests

add zero_ne_add_one

045ff14

fix

e3fc34f

kim-em force-pushed the simp_succ_eq_add_one branch from 725360d to e3fc34f Compare March 13, 2024 03:28

fixes

c1f3440

github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 13, 2024 03:47 Inactive

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 13, 2024

Trigger CI for leanprover/lean4#3579

c59e73d

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 13, 2024

Trigger CI for leanprover/lean4#3579

801ffd9

kim-em added this pull request to the merge queue Mar 13, 2024

Merged via the queue into master with commit 317adf4 Mar 13, 2024
22 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream #3579

chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream #3579

kim-em commented Mar 3, 2024

leanprover-community-mathlib4-bot commented Mar 4, 2024 •

edited

Loading

chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream #3579

chore: add @[simp] to Nat.succ_eq_add_one, and cleanup downstream #3579

Conversation

kim-em commented Mar 3, 2024

leanprover-community-mathlib4-bot commented Mar 4, 2024 • edited Loading

leanprover-community-mathlib4-bot commented Mar 4, 2024 •

edited

Loading