Ana de Almeida Borges (Oct 25 2022 at 17:48): Ana de Almeida Borges (Oct 25 2022 at 17:48):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?
Karl Palmskog (Oct 25 2022 at 18:12):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)
Paolo Giarrusso (Oct 25 2022 at 23:53):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
Paolo Giarrusso (Oct 25 2022 at 23:55):The code in Ana's link looks hand-written, but the maths and notations are in autosubst's style
Dominik Kirst (Oct 26 2022 at 07:29):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.
Ana de Almeida Borges (Oct 26 2022 at 12:42):Cool, thanks everyone
Notification Bot (Oct 26 2022 at 12:42):Ana de Almeida Borges has marked this topic as resolved.
Last updated: Oct 04 2023 at 23:01 UTC