coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A coercion doesn't work

From: Victor Porton <porton AT narod.ru>
To: coq-club Club <coq-club AT inria.fr>
Subject: [Coq-Club] A coercion doesn't work
Date: Wed, 14 Aug 2013 21:12:06 +0300
Envelope-from: porton AT yandex.ru

[[[
Inductive QF := qf.

Definition f := fun _:nat => 0.

Definition convert(x:QF) := f.

Definition F := nat->nat.

Coercion convert : QF >-> F.
]]]

gives error message:

Error: Found target class F instead of Funclass.

Why it does not work? What is wrong?

--
Victor Porton - http://portonvictor.org

[Coq-Club] A coercion doesn't work, Victor Porton, 08/14/2013