class Zero (α : Type u) where
zero : α
class AddZeroClass (M : Type u) extends Zero M, Add M
class AddMonoid (M : Type u) extends AddZeroClass M where
nsmul : Nat → M → M := fun _ _ => Zero.zero
class AddCommMonoid (M : Type u) extends Zero M, AddMonoid M
class AddMonoidWithOne (R : Type u) extends AddMonoid R
class AddCommMonoidWithOne (R : Type u) extends AddMonoidWithOne R, AddCommMonoid R
class NonAssocSemiring (α : Type u) extends Zero α, AddCommMonoidWithOne α
class Semiring (α : Type u) extends Zero α, NonAssocSemiring α
-- ignoring default value for field 'nsmul'
The last class declaration unexpectedly produces the above warning, with no apparent way to fix it. Declaring the default value again in Semiring does not help either.
The last class declaration unexpectedly produces the above warning, with no apparent way to fix it. Declaring the default value again in
Semiringdoes not help either.