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: Mar 03 2024 at 16:02 UTC