Stream: hs-to-coq devs & users

Topic: GADTs

view this post on Zulip Pedro Abreu (Aug 23 2021 at 18:15):

quick question: does hs-to-coq support GADTs?

view this post on Zulip Stephanie Weirich (Aug 24 2021 at 01:36):

i don’t think so.

--Stephanie

view this post on Zulip Yao Li (Sep 03 2021 at 20:29):

@Pedro Abreu Sorry I wasn't paying attention to Zullip. I actually added some heuristics to support some instances of GADTs some time ago (see: https://github.com/plclub/hs-to-coq/blob/master/examples/tests/GADT.hs), but I don't think it supports all GADTs.

Last updated: Feb 06 2023 at 07:03 UTC