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?
You can, the command is tmExistingInstance
: https://github.com/MetaCoq/metacoq/blob/coq-8.16/template-coq/theories/TemplateMonad/Core.v#L62
You first define your instance using tmDefinition,
and then call tmExistingInstance
(so it's two commands rather than one)
ooh so that's what that is. Thanks!
Last updated: Jun 01 2023 at 13:01 UTC