coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Claudio Sacerdoti Coen <sacerdot AT cs.unibo.it>
- To: Pierre Casteran <pierre.casteran AT labri.fr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Example of functor type
- Date: Fri, 18 Feb 2005 10:55:05 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
> By the way, it is possible that the following is a bad use of
> functor types :-(
I forgot to add: yes, basically it is. I have not found yet any
use for functor types. What you want to do is probably:
Module Type S1.
Parameter t : Set.
Parameter eq_dec : forall a b:t, {a=b}+{a<>b}.
End S1.
Module Type S2 (M:S1).
Declare Module 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.
Module F1_2 (M:S1) : S2 with Module M := M.
--
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail:
sacerdot AT cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------
- [Coq-Club] Example of functor type, Pierre Casteran
- Re: [Coq-Club] Example of functor type, Claudio Sacerdoti Coen
- Re: [Coq-Club] Example of functor type, Claudio Sacerdoti Coen
Archive powered by MhonArc 2.6.16.