Michael Soegtrop (Feb 25 2021 at 11:49): Michael Soegtrop (Feb 25 2021 at 11:49):@Pierre-Marie Pédrot : I created a stream for Ltac2 and took the freedom to subscribe you to it.
I wanted to continue the discussion on the $ notation for trivial anti quotations and the hiding of this notation by CompCert. It is quite hard to get around importing the notation and using an ltac2 function for this is a bit less efficient as you said and also not that readable. Also asking CompCert to change this doesn't make much sense - it is legitimate to define such a notation.
I wonder if we can have a syntax like ltac2var:(x) in addition to $x. I might even prefer that form, because it makes the code more readable to less proficient users (at least if one doesn't have 10 anti quotations in one line).
Michael Soegtrop (Feb 26 2021 at 11:10):I thought a bit more about it. I think we should have two forms of the ltac2: anti quotation - one as is which is expected to be of type unit and is evaluated for its side effects, and another one which is expected to return a constr term. And I think ltac2: should give a warning if the return type is not unit.
Last updated: May 31 2023 at 04:01 UTC