Skip to content

Commit

Permalink
chore: bump std to 604b407, catching up to leanprover-community/batte…
Browse files Browse the repository at this point in the history
…ries#361 (#8959)

Co-authored-by: Tobias Grosser <tobias@grosser.es>
Co-authored-by: James <jamesgallicchio@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Siddharth Bhat <siddu.druid@gmail.com>
  • Loading branch information
6 people committed Dec 11, 2023
1 parent bacd2ec commit 193e156
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 4 deletions.
3 changes: 0 additions & 3 deletions Mathlib/Data/Int/Basic.lean
Expand Up @@ -140,9 +140,6 @@ theorem sign_coe_add_one (n : ℕ) : Int.sign (n + 1) = 1 :=
rfl
#align int.sign_coe_add_one Int.sign_coe_add_one

@[simp]
theorem sign_negSucc (n : ℕ) : Int.sign -[n+1] = -1 :=
rfl
#align int.sign_neg_succ_of_nat Int.sign_negSucc

/-! ### succ and pred -/
Expand Down
2 changes: 1 addition & 1 deletion lake-manifest.json
Expand Up @@ -4,7 +4,7 @@
[{"url": "https://github.com/leanprover/std4",
"type": "git",
"subDir": null,
"rev": "b197bd218dbab248ad8899404334d41da04f5d13",
"rev": "604b4078d46104d4144a87ebf4c2dae581cb704a",
"name": "std",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand Down

0 comments on commit 193e156

Please sign in to comment.