coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coercions and Defined Types

From: Gregory Malecha <gmalecha AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Coercions and Defined Types
Date: Thu, 1 Oct 2015 15:53:45 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-yk0-f170.google.com
Ironport-phdr: 9a23:caQP6BWnrHbWTf3NGNBgnR//bJTV8LGtZVwlr6E/grcLSJyIuqrYZhOHt8tkgFKBZ4jH8fUM07OQ6PC8HzJbqs/f+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8GVPV4D3WT1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S43VXxeuR5VCUCR5xbjG5z1ryHSt+xn2SDcM9egHp4uXjH3wL1mRxjymW8iPjo0+2Hewph/iatfrRmhrjRwxofVZMeeM/8oLfCVRs8TWWcUBpUZbCdGGI7pKtJXV+c=

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

[Coq-Club] Coercions and Defined Types, Gregory Malecha, 10/02/2015
- Re: [Coq-Club] Coercions and Defined Types, Jason Gross, 10/02/2015
  - Re: [Coq-Club] Coercions and Defined Types, Gregory Malecha, 10/02/2015
    - Re: [Coq-Club] Coercions and Defined Types, Jason Gross, 10/02/2015