Stream: MetaCoq

Topic: Typeclasses


view this post on Zulip Pedro Abreu (Jun 28 2022 at 12:21):

Hi, I would like to declare a type class instance through the TemplateMonad but it seems that this is not currently doable, is that correct? In this case, Is there something more fundamental to why it's not possible or it's just something that is not implemented yet?

view this post on Zulip Yannick Forster (Jun 28 2022 at 12:22):

You can, the command is tmExistingInstance: https://github.com/MetaCoq/metacoq/blob/coq-8.16/template-coq/theories/TemplateMonad/Core.v#L62

view this post on Zulip Yannick Forster (Jun 28 2022 at 12:22):

You first define your instance using tmDefinition, and then call tmExistingInstance (so it's two commands rather than one)

view this post on Zulip Pedro Abreu (Jun 28 2022 at 12:35):

ooh so that's what that is. Thanks!


Last updated: Aug 11 2022 at 03:02 UTC