The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Dear All,

I am trying to define a Coercion inside a Module. When trying to use
this Coercion outside the Module, it seems to be running into trouble.
See example below. Is it possible to define a Coercion inside a module
that accepts something from the Module Type and use it outside the
Module?

Kind Regards,
Chris


Module Type ModType.
   Axiom S: Set.
   Axiom T: Set.
End ModType.

Module Mod (M: ModType).
   Export M.
   Axiom f: S -> T.
   Coercion f: S >-> T.
End Mod.

Module ModTypeImpl <: ModType.
   Definition S: Set := nat.
   Definition T: Set := bool.
End ModTypeImpl.

Module ModImpl := Mod ModTypeImpl.
Import ModImpl.

(* Error: The term "1" has type "nat" while it is expected to have
type "bool". *)
(* Check negb 1. *)

Definition ff: nat -> bool := f.
Coercion ff: nat >-> bool.

(* No error: apparently it was made to work with the coercion ff,
which is defined
   to be f. But f was also made a coercion above in Mod. *)
Check negb 1.