The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is it possible to reuse definitions from a module type?  That is, is there any way to get around giving the body of [bar] in [foo'] (which needs to match the definition of [bar] in [foo] anyway) in the following?

Module Type foo.

  Axiom A : Type.

  Definition bar : forall x : A, x = x := fun _ => eq_refl.

End foo.

Module foo' : foo.

  Definition A := False.

  (*Definition bar : forall x : A, x = x := fun x => match x with end.*)

(* Error: Signature components for label bar do not match:

the body of definitions differs. *)

End foo'.

(* Error: The field bar is missing in Top.foo'. *)

Thanks,

Jason