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):

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

Last updated: Jun 25 2024 at 14:01 UTC