Skip to content

Commit

Permalink
chore: bump std4 (#2946)
Browse files Browse the repository at this point in the history
We bump std4 and take care to delete the now-upstreamed (leanprover-community/batteries#107) instances mentioned in #2878.
  • Loading branch information
thorimur committed Mar 17, 2023
1 parent 3fdd077 commit 8decdf8
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 10 deletions.
9 changes: 0 additions & 9 deletions Mathlib/Data/Nat/Cast/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -39,15 +39,6 @@ protected def Nat.unaryCast {R : Type u} [One R] [Zero R] [Add R] : ℕ → R

#align nat.cast Nat.cast

-- see note [coercion into rings]
instance [NatCast R] : CoeTail ℕ R where coe := Nat.cast

-- see note [coercion into rings]
instance [NatCast R] : CoeHTCT ℕ R where coe := Nat.cast

/-- This instance is needed to ensure that `instCoeNatInt` is not used. -/
instance : Coe ℕ ℤ where coe := Nat.cast

-- the following four declarations are not in mathlib3 and are relevant to the way numeric
-- literals are handled in Lean 4.

Expand Down
2 changes: 1 addition & 1 deletion lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,6 @@
{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
"rev": "44a92d84c31a88b9af9329a441890ad449d8cd5f",
"rev": "d4107bc2bd28bc70e8327578c16acb904d2bcfd0",
"name": "std",
"inputRev?": "main"}}]}

0 comments on commit 8decdf8

Please sign in to comment.