Zulip Chat Archive

Stream: new members

Topic: widget component example


view this post on Zulip Angela Li (Dec 29 2020 at 01:22):

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.

view this post on Zulip Bryan Gin-ge Chen (Dec 29 2020 at 01:52):

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

view this post on Zulip Edward Ayers (Dec 31 2020 at 10:09):

Hello, I think that I made a mistake with typeclasses

view this post on Zulip Edward Ayers (Dec 31 2020 at 10:16):

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.

view this post on Zulip Bryan Gin-ge Chen (Dec 31 2020 at 18:55):

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


Last updated: May 14 2021 at 00:42 UTC