tests/lean/diamond8.lean.expected.out - third_party/github.com/leanprover/lean4 - Git at Google


            
            inductive Semiring.{u} : Type u → Type u

            
            number of parameters: 1

            
            constructors:

            
            Semiring.mk : {R : Type u} → [toAddCommMonoid : AddCommMonoid R] → [toMonoid : Monoid R] → Semiring R
	inductive Semiring.{u} : Type u → Type u
	number of parameters: 1
	constructors:
	Semiring.mk : {R : Type u} → [toAddCommMonoid : AddCommMonoid R] → [toMonoid : Monoid R] → Semiring R