coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Questions about "Declare ML Module" etc, austin.zhuang
- Re: [Coq-Club] Questions about "Declare ML Module" etc, Guillaume Yziquel
Archive powered by MhonArc 2.6.16.