Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Questions about "Declare ML Module" etc

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Questions about "Declare ML Module" etc


chronological Thread 
  • From: Guillaume Yziquel <guillaume.yziquel AT citycable.ch>
  • To: "austin.zhuang" <dyzz AT mail.ustc.edu.cn>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Questions about "Declare ML Module" etc
  • Date: Wed, 19 Nov 2008 23:54:46 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

austin.zhuang a écrit :
>
>     for example, I have "lib.ml":
>       type data_type = |INT|FLOAT|DOUBLE
>     
>     How can I use this data_type definition in Coq? And Can I use functions
> in ".cmo" file or even more?

This is a question I'd also be very interested in.

Guillaume Yziquel.





Archive powered by MhonArc 2.6.16.

Top of Page