Implicit Arguments · Hydras & Co. universe

In the old goedel+Ackermann library, the same constructor of the abstract syntax of FOL formula had various representations, depending of the considered module. Some redefinitions like Definition forallH := forallH LNN. resulted in some issues (complex proof scripts, difficulty to design simple notations, etc.)
In the branch Implicits, I propose a uniform abstract syntax using implicit arguments, and fix the changes in proof scripts. After some minor changes (mainly comments + indentation) , I plan to merge it intomaster`.

Karl Palmskog (Feb 24 2023 at 18:30):

sounds good, let us know if any help is needed with the PR/branch. I think Coq 8.17.0 is coming out soon finally, but it should work fine with CI and so on.

Pierre Castéran (Feb 24 2023 at 18:41):

Ok, next week, I will try to improve the presentation, and submit a draft PR.

Pierre Castéran (Feb 25 2023 at 17:35):

I made a draft PR. Works, except in dev (because of Equations, probably).

Karl Palmskog (Feb 25 2023 at 17:44):

hmm, one thing that comes to mind is that I believe one can locally clear implicit arguments (to avoid having a lot of @ somewhere)

Karl Palmskog (Feb 25 2023 at 17:49):

e.g., #[local] Arguments validator_state _ _ : clear implicits.

Karl Palmskog (Feb 25 2023 at 17:52):

hmm, the Equations brekage is strange, I didn't get it locally. There may be an issue with the master Docker image, but I'll wait for a day before reporting to Coq-Docker. (Image should be rebuilt overnight)