Pedro Abreu (Jun 28 2022 at 12:21): 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?
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
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)
Pedro Abreu (Jun 28 2022 at 12:35):ooh so that's what that is. Thanks!
Last updated: Jun 01 2023 at 13:01 UTC