\import Algebra.Monoid
\import Algebra.Monoid.Sub
\import Algebra.Semiring
\import Paths.Meta

\class SubPseudoSemiring \extends SubAddMonoid, SubSemigroup {
  \override S : PseudoSemiring

  \func IPseudoSemiring : PseudoSemiring \cowith
    | AbMonoid => SubAddMonoid.abStruct \this
    | Semigroup => ISemigroup
    | ldistr => ext ldistr
    | rdistr => ext rdistr
    | zro_*-left => ext zro_*-left
    | zro_*-right => ext zro_*-right
} \where {
  \func cStruct {R : PseudoCSemiring} (S : SubPseudoSemiring R) : PseudoCSemiring \cowith
    | PseudoSemiring => S.IPseudoSemiring
    | *-comm => ext *-comm

}

\class SubSemiring \extends SubPseudoSemiring, SubMonoid {
  \override S : Semiring

  \func ISemiring : Semiring \cowith
    | PseudoSemiring => IPseudoSemiring
    | Monoid => IMonoid
} \where {
  \func cStruct {R : CSemiring} (S : SubSemiring R) : CSemiring \cowith
    | Semiring => S.ISemiring
    | PseudoCSemiring => SubPseudoSemiring.cStruct S

  \func max {A : Semiring} : SubSemiring \cowith
    | SubAddMonoid => SubAddMonoid.max {A}
    | SubMonoid => SubMonoid.max
}