Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Example of functor type

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Example of functor type


chronological Thread 
  • 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
----------------------------------------------------------------




Archive powered by MhonArc 2.6.16.

Top of Page