/metaprogramming-rosetta-stone

A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming languages [maintainer=@yforster]

Primary LanguageCoqMIT LicenseMIT

Rosetta stone of metaprogramming in Coq

Contributing Code of Conduct Zulip

Meta

  • Author(s):
    • Enzo Crance
    • Davide Fissore
    • Yannick Forster
    • Gaëtan Gilbert
    • Talia Ringer
    • Michael Soegtrop
    • Enrico Tassi
    • Tomas Vallejos
  • Coq-community maintainer(s):
  • License: MIT License
  • Compatible Coq versions: 8.17
  • Additional dependencies: multiple, see READMEs in directories