coq - 使用 Coq 中的“递归提取”提取到 OCaml 文件

Question

我想将一个函数提取foo到Coq一个OCaml文件中。因为我真正的函数必须使用 . Recursive Extraction，所以当我运行程序时，它会在cmd. 但我想将其输出到文件中，例如：foo.ml

Recursive Extraction foo.

当我尝试时：

Recursive Extraction "foo.ml" foo.

或者Recursive Extraction foo "foo.ml"

我收到一个错误：Syntax error: "." expected after [vernac:command] (in [vernac_aux]).

我的问题是：我是否能够foo使用Recursive Extraction语法将函数提取到文件中？谢谢您的帮助。

Answer 1

根据手册（http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual027.html），Extraction "foo.ml" foo将提取foo并递归其所有依赖项到foo.ml，即在这种情况下您不需要Recursive它仅用于标准输出上的提取。