diff --git a/doc/typeclass.md b/doc/typeclass.md index a26ee0cfac..4f8c1a6623 100644 --- a/doc/typeclass.md +++ b/doc/typeclass.md @@ -343,11 +343,6 @@ class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where export HMul (hMul) -class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where - hMul : α → β → γ - -export HMul (hMul) - instance : HMul Nat Nat Nat where hMul := Nat.mul @@ -464,4 +459,4 @@ TODO ## Local Instances -TODO \ No newline at end of file +TODO