The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hi, Jason --

Thanks for the pointer. I think it would have worked, except my example a little bit more simplified since [a] and [b] need associated type class instances. So the type of [onEach] is really [forall a b, X a -> Y b -> foo a b -> bar a b]. Coq reports that this does not respect the uniform inheritence condition, which is in line with what is written in the manual.

On Thu, Oct 1, 2015 at 4:12 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

As a kludge, stick the definitions in a module, their types in a module type, declare the coercion in a functor, and then import the applied functor?

-Jason

On Oct 1, 2015 6:54 PM, "Gregory Malecha" <gmalecha AT gmail.com> wrote:

Hello --

I have some types (similar to):

Definition foo a b  := list a -> b.

Definition bar a b := a -> b.

and I have a function to transport [foo]s into [bar]s.

Definition onEach : forall a b, foo a b -> bar a b.

I want to declare [onEach] as a coercion:

Coercion onEach : foo >-> bar.

but I get

Error: Found target class bar instead of Funclass.

Is there some way to tell Coq that it should treat [bar] as opaque? I know that I can make [bar] a record type, but I don't really want to pack and unpack functions all the time.

Thanks.

--

gregory malecha

--

gregory malecha