The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hello,

 I am looking for a (simple if possible) example of a functor type
(as created with "Module Type ident module_bindings := module_type")
and how to apply this functor.

By the way, it is possible that the following is a bad use of
functor types :-(


Pierre



Module Type S1.
 Parameter t : Set.
 Parameter eq_dec : forall a b:t, {a=b}+{a<>b}.
End S1.

Module Type S2 (M:S1).
 Definition t := M.t.
 Definition eq_dec := M.eq_dec.
 Parameter eq_dec_prop : forall a b:t, a = b \/ a <> b.
End S2.

(*
 all the following commands raise errors.


Module F1_2 (M:S1) : S2.

Module F1_2 (M:S1) : S2 with Module M:=M.

Module F1_2 (M:S1) : S2 M.

Module F1_2 (M:S1) : (S2 M).

*)


-- 
Pierre Casteran
(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.