From 994a5b55dce52e717d0a21adecd807c2c026fa17 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 2 Sep 2024 17:38:49 +1000 Subject: [PATCH] cleanup tests --- tests/lean/run/structWithAlgTCSynth.lean | 6 ------ tests/lean/run/synthInstsIssue.lean | 12 ------------ 2 files changed, 18 deletions(-) diff --git a/tests/lean/run/structWithAlgTCSynth.lean b/tests/lean/run/structWithAlgTCSynth.lean index d4d16c39d4d6..4fae68c94cf6 100644 --- a/tests/lean/run/structWithAlgTCSynth.lean +++ b/tests/lean/run/structWithAlgTCSynth.lean @@ -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 : α diff --git a/tests/lean/run/synthInstsIssue.lean b/tests/lean/run/synthInstsIssue.lean index 6681cdb9b6ed..b64601231646 100644 --- a/tests/lean/run/synthInstsIssue.lean +++ b/tests/lean/run/synthInstsIssue.lean @@ -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