Skip to content

leque/coq-to-lisp

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

2 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Convert Coq to Scheme Extraction to Common Lisp / Emacs Lisp, and auxiliary macros for them.

Requirement

R7RS Scheme implementation.

You may run unschme-impl.scm on R5RS Scheme implementation with some additional procedures:

  • error
  • command-line
  • exit
  • current-error-port

How to use.

Extract Scheme code.

% coqc example.v

Convert extracted code to Common Lisp / Emacs Lisp. For example, with chibi-scheme,

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

or

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

Output format is automatically determined by the file extension.

And run.

% sbcl --load macros_extr.lisp --load example.lisp --script test.lisp

About

Coq to Emacs Lisp / Common Lisp Extraction

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published