widget component example

Stream: new members

[Angela Li]

Hello. I am looking at https://leanprover-community.github.io/mathlib_docs/init/meta/widget/basic.html.

meta def Hello : component string α := component.pure (λ s, ["hello, ", s, ", good day!"])
#html Hello "lean" -- renders "hello, lean, good day!"

I got it to work with

meta def Hello : component string empty := component.pure (λ s, ["hello, ", s, ", good day!"])
#html html.of_component "lean" Hello -- renders "hello, lean, good day!"

but I'm confused why

meta def Hello : component string empty := component.pure (λ s, ["hello, ", s, ", good day!"])
#html Hello "lean" -- renders "hello, lean, good day!"

gives this error

maximum class-instance resolution depth has been reached
(the limit can be increased by setting option 'class.instance_max_depth')
(the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

Thanks.

[Bryan Gin-ge Chen]

The documentation there might be out of date. cc: @Edward Ayers

[Edward Ayers]

Hello, I think that I made a mistake with typeclasses

[Edward Ayers]

So the problem is that when you write Hello "lean", there is a function coercion, but the typeclass inference system is getting stuck in a loop for some reason. I suggest that you just use the clunkier version with html.of_component for now. Maybe someone who actually understands typeclasses knows what needs to change to get this to work.

[Bryan Gin-ge Chen]

@Edward Ayers thanks for the explanation! I've opened lean#512 for now.