max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix doc

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-06 19:55:31 -07:00
parent ddae76aed2
commit 2494f1d4a4
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/typeclass.md
View file

@ -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.