Jason Gross (Nov 28 2022 at 19:26): 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: May 31 2023 at 03:30 UTC