coq to lisp:Coq到Emacs Lisp通用Lisp提取

将Coq到Scheme Extraction转换为Common Lisp / Emacs Lisp，以及它们的辅助宏。要求R7RS方案实施。您可以在R5RS Scheme实现上运行unschme-impl.scm并使用一些附加程序：错误命令行出口当前错误端口如何使用。提取方案代码。提取的代码可以通过以下命令转换为Common Lisp / Emacs Lisp：

% coqc example.v

例如，使用以下命令：

% chibi-scheme unscheme.scm example.lisp 或 % chibi-scheme unscheme.scm example.el

输出格式由文件扩展名自动确定。您还可以运行：

% sbcl --load macros_extr.lisp --load exa