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):

https://github.com/leanprover-community/mathlib/blob/kbuzzard_typeclass_inference_doc/docs/extras/typeclass_inference.md

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: Aug 03 2023 at 10:10 UTC