Zulip Chat Archive
Stream: general
Topic: TC inference explanation
Yaël Dillies (Apr 06 2022 at 14:23):
Are people interested in having Kevin's TC inference explanation on the website somewhere? It's WIP over at branch#kbuzzard_typeclass_inference_doc.
Patrick Massot (Apr 06 2022 at 14:26):
What is Kevin's explanation?
Yaël Dillies (Apr 06 2022 at 14:26):
cf the branch
Patrick Massot (Apr 06 2022 at 14:26):
I tried
Patrick Massot (Apr 06 2022 at 14:26):
Could you link to either a file or a commit?
Yaël Dillies (Apr 06 2022 at 14:28):
Eric Wieser (Apr 06 2022 at 14:33):
Probably that stuff belongs on the leanprover-community website not the mathlib docs
Eric Wieser (Apr 06 2022 at 14:33):
(you'll note everything else in that directory is a stub file indicating the content has moved)
Yaël Dillies (Apr 06 2022 at 14:34):
Yes sorry, that's what I meant by "the website".
Yaël Dillies (Apr 06 2022 at 14:34):
Kevin wrote that in the old time of when the website was still in that folder.
Eric Rodriguez (Apr 06 2022 at 14:40):
(the FAQ is still there on my github, btw! maybe worth putting in there)
Patrick Massot (Apr 06 2022 at 14:58):
Yaël, what do you see in that document that is not covered in the standard sources (except for the TODO list at the end)?
Yaël Dillies (Apr 06 2022 at 19:36):
Don't know. I am just asking.
Last updated: Dec 20 2023 at 11:08 UTC