From 2494f1d4a40f01a0402da4fc2153462289f5eaff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Jul 2022 19:55:31 -0700 Subject: [PATCH] chore: fix doc --- doc/typeclass.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/typeclass.md b/doc/typeclass.md index a7d6cfb35f..bf36e0e34c 100644 --- a/doc/typeclass.md +++ b/doc/typeclass.md @@ -353,9 +353,9 @@ instance : HMul Int Int Int where def xs : List Int := [1, 2, 3] +# -- TODO: fix error message -- Error "failed to create type class instance for HMul Int ?m.1767 (?m.1797 x)" -# -- FIXME: should fail -#check fun y => xs.map (fun x => hMul x y) +-- #check fun y => xs.map (fun x => hMul x y) # end Ex ``` The instance `HMul` is not synthesized by Lean because the type of `y` has not been provided.