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 into master`.
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.
Ok, next week, I will try to improve the presentation, and submit a draft PR.
I made a draft PR. Works, except in dev (because of Equations, probably).
hmm, one thing that comes to mind is that I believe one can locally clear implicit arguments (to avoid having a lot of
#[local] Arguments validator_state _ _ : clear implicits.
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)
OK, I could remove the "@" in LNT.v
I'll try to do it tomorrow (the "fol." prefix too).
I figured out the CI issues, unfortunately the workaround I pushed in the
Implicits branch makes CI take longer than usual
I removed a lot (all ???) of "fol." prefix in front of abstract syntax constructors.
looks reasonable to merge now to me
Last updated: Jun 10 2023 at 23:01 UTC