Yannick Forster said:

Depending on your use case, Autosubst 2 might be better to use than Autosubst 1. We are using it in the Coq Library of Undecidability to formalise first-order logic, second-order logic, STLC, and System F

Does this mean that, eg, the FOL syntax file is somehow auto-generated? Or where/how are you using Autosubst 2 in the Library of Undecidability?

Autosubst 2 is written in Haskell and generates Coq code in the end that needs to be bundled, but I guess one can autogenerate it every time in CI... (so I don't know if that particular file is autogenerated)

https://github.com/uds-psl/coq-library-undecidability/blob/6207468f34c21c1c07b391f02bd51e33a7553f86/theories/SystemF/Autosubst/syntax.v is much closer to the autogen output I've seen from Autosubst 2. https://github.com/uds-psl/coq-library-undecidability/search?q=autosubst finds more examples

The code in Ana's link looks hand-written, but the maths and notations are in autosubst's style

Paolo Giarrusso said:

The code in Ana's link looks hand-written, but the maths and notations are in autosubst's style

Exactly, the FOL syntax is Autosubst inspired and the System F syntax is really Autosubst generated. Another example of Autosubst generated code in the undecidability library is the syntax used for higher order unification.

Cool, thanks everyone

Ana de Almeida Borges has marked this topic as resolved.

Last updated: Jan 28 2023 at 06:30 UTC