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

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

  \func struct : Semiring \cowith
    | AbMonoid => SubAddMonoid.abStruct \this
    | Monoid => SubMonoid.struct
    | ldistr => ext ldistr
    | rdistr => ext rdistr
    | zro_*-left => ext zro_*-left
    | zro_*-right => ext zro_*-right
} \where {
  \func cStruct {R : CSemiring} (S : SubSemiring R) : CSemiring \cowith
    | Semiring => S.struct
    | *-comm => ext *-comm

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