From 2afbb2ce4273c87a8d68e258db29250640c19119 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 9 Dec 2020 11:07:02 +0100 Subject: [PATCH] doc: fix --- doc/typeclass.md | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) 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