/metaprogrammable-editor

Documents (TeX, slides etc.) and code for the editor side metaprogramming in Coq.

Primary LanguageTeX

metaprogrammable-editor

Documents (TeX, slides etc.) and code for the editor side metaprogramming in Coq.

This provides a simple mechanism to write Emacs editor macros in Coq, using the monadic embedded domain-specific language. We can then run them in Emacs, using the interpreter written in Emacs Lisp.

Screencast