Zulip Chat Archive

Stream: lean4

Topic: Impossible to pass Type1 GADT in IO

Schrodinger ZHU Yifan (Sep 10 2023 at 13:55):

Is this by design?

Kevin Buzzard (Sep 10 2023 at 14:00):

Is this discussion relevant? Disclaimer: I don't know anything about this stuff, I just remembered that it had been discussed at least once before. Hope I'm not creating noise.

James Gallicchio (Sep 10 2023 at 14:03):

nope, pretty sure that's the right thread

James Gallicchio (Sep 10 2023 at 14:04):

actually there might be another thread that talks about it, let me search...

James Gallicchio (Sep 10 2023 at 14:11):

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/universe.20polymorphic.20IO this has a bunch of discussion as well

Schrodinger ZHU Yifan (Sep 10 2023 at 15:23):

Thanks! The information is helpful.

Last updated: Dec 20 2023 at 11:08 UTC