The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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