Metaprogramming defunctionalization in Rocq
This is a prototype to metaprogram defunctionalization in the Rocq proof assistant.
It compiles with Rocq 9.0.0 and Rocq-Elpi 2.5.2, using the following
command in the src directory:
rocq compile Defun.v
It is released under the GNU GPL license v3 (see LICENSE) for details.
Authors:
- Chantal Keller, LMF, Université Paris-Saclay
- Camille Noûs, Laboratoire Cogitamus, Université publique