Stream: Coq users

Topic: Coercion to specific Funclass?


view this post on Zulip Joshua Grosso (May 09 2021 at 18:49):

Is there a way to make a Coercion to a function of a specific type, other than just Funclass as a whole? (I'd like to make multiple Coercions depending on the types of the functions, which are completely unambiguous, but I can't figure out how.)

view this post on Zulip Gaƫtan Gilbert (May 09 2021 at 19:20):

no
we don't know the type of the function when we coerce


Last updated: Jan 28 2023 at 05:02 UTC