Stream: MetaCoq

Topic: tmExistingInstance

view this post on Zulip Jason Gross (Feb 24 2023 at 03:16):

Why is tmExistingInstance #[local] in the extractable monad, but #[global] in the core monad?

view this post on Zulip Matthieu Sozeau (Feb 24 2023 at 15:51):

Another discrepancy, sorry

view this post on Zulip Jason Gross (Feb 28 2023 at 04:40):

I submitted a PR at https://github.com/MetaCoq/metacoq/pull/857 to generalize tmExistingInstance to allow the user to specify the locality

Last updated: Apr 20 2024 at 14:01 UTC