Извлечь в файл OCaml с помощью "Рекурсивное извлечение" в Coq

Question

Я хочу извлечь функцию foo в Coq для OCaml файл. Потому что моя настоящая функция должна использовать Recursive ExtractionКогда я запускаю программу, она выводит извлеченный код OCaml на 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 в этом случае он используется только для извлечения на стандартный вывод.