Stream: MetaCoq

Topic: Template Monad universes


view this post on Zulip Jason Gross (Nov 28 2022 at 19:26):

Why does TemplateMonad in template-coq/theories/TemplateMonad/Core.v have two explicit universe arguments but one of them is constrained to be equal to the monomorphic universe option_instance.u0? (The constraint comes from Monomorphic Inductive option_instance whose source and target are constrained to live in the same universe.)


Last updated: Feb 04 2023 at 02:03 UTC