Skip to content

Commit

Permalink
cleanup tests
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Sep 10, 2024
1 parent eb8cf99 commit 994a5b5
Show file tree
Hide file tree
Showing 2 changed files with 0 additions and 18 deletions.
6 changes: 0 additions & 6 deletions tests/lean/run/structWithAlgTCSynth.lean
Original file line number Diff line number Diff line change
Expand Up @@ -87,12 +87,6 @@ end Mathlib.Data.Quot

section Mathlib.Init.ZeroOne

class Zero.{u} (α : Type u) where
zero : α

instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
ofNat := ‹Zero α›.1

class One (α : Type u) where
one : α

Expand Down
12 changes: 0 additions & 12 deletions tests/lean/run/synthInstsIssue.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,18 +4,6 @@ https://github.com/leanprover/lean4/pull/2793.
We find that we need to either specify a named argument or use `..` in certain rewrites.
-/

section Mathlib.Init.ZeroOne

set_option autoImplicit true

class Zero.{u} (α : Type u) where
zero : α

instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
ofNat := ‹Zero α›.1

end Mathlib.Init.ZeroOne

section Mathlib.Algebra.Group.Defs

universe u v w
Expand Down

0 comments on commit 994a5b5

Please sign in to comment.