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


            
            constructor Ring.mk.{u} : {R : Type u} → [toZero : Zero R] → (gsmul : Int → R → R) → (∀ (a : R), gsmul 0 a = 0) → Ring R

            
            Ring.mk (fun x n => x.toNat * n) ⋯ : Ring Nat
	constructor Ring.mk.{u} : {R : Type u} → [toZero : Zero R] → (gsmul : Int → R → R) → (∀ (a : R), gsmul 0 a = 0) → Ring R
	Ring.mk (fun x n => x.toNat * n) ⋯ : Ring Nat