tchajed
Lazy list explanation
You refer here to some comments in the Ltac2 documentation which are not easy to understand.
https://github.com/tchajed/ltac2-tutorial/blob/ce5b3536efa1e73cf580178b03cd5acdb8d9426e/src/ltac2_tutorial.v#L358
I agree with you, I also found them difficult to understand.
After thinking about it for a while I started to make more sense of it. I wrote up my comments in a git PR for the Coq documentation. https://github.com/coq/coq/pull/19470/files
However, it will take a while of discussion with developers and approval for things like this to get merged, the semantics have to be precisely correct and all that. Still, I believe that my insights will be valuable. Would you read through this PR I linked and consider incorporating some of the comments into your own repository?
You can use the text verbatim if you are happy with the wording, otherwise feel free to reword it as you see fit. I can create a PR for this repo if that would be easier, I just thought you might prefer to phrase it as you see most clear/readable.
