Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: "austin.zhuang" <dyzz AT mail.ustc.edu.cn>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] Questions about "Declare ML Module" etc
  • Date: Mon, 17 Nov 2008 05:00:37 -0800 (PST)
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,
   I just read about extraction and was interested in how to use ocaml code
in Coq. I find "Declare ML Module" in reference manual, which is a way to
load ".cmo" file. But there is no more guides in the manual, so, can anyone
give a quick example of this?
  
    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?
    
    p.s. Would there be a part of how to write coq tactics in ocaml in the
future?
  
    Thanks!
                                                                              
                      
Austin Zhuang
                                                                              
                       
SSG@USTC
                                                                              
                    
-- 
View this message in context: 
http://www.nabble.com/Questions-about-%22Declare-ML-Module%22-etc-tp20538966p20538966.html
Sent from the Coq mailing list archive at Nabble.com.





Archive powered by MhonArc 2.6.16.

Top of Page