Lutz Wrage (May 22 2021 at 22:25): Lutz Wrage (May 22 2021 at 22:25):Is there any tutorial available for creating non-trivial notations? I've tried to read through the reference, but I find it quite hard to learn from it.
Yannick Forster (May 23 2021 at 11:15):In my experience, learning how to write notations works best by looking at what other people have done, and then lots of learning by doing (and failing). For what kind of language / mathematics do you want to write notations? Somebody might then be able to point you in a direction where somebody else wrote notations for something similar
Paolo Giarrusso (May 23 2021 at 12:50):It also helps to understand how LL(1) parsing works, and the Camlp5 manual. You can't write an LL(1) grammar without understanding a bit on the implementation, and using Coq notations is no easier. After that, most things become much easier (tho I wouldn’t say “easy”).
Paolo Giarrusso (May 23 2021 at 12:52):I want to say “there are lots of explanations about left factoring” (which is one of the FAQs), but I didn’t find anything great last time it came up and I googled (that is, this week)…
Cody Roux (May 23 2021 at 15:55):Yannick Forster said:
In my experience, learning how to write notations works best by looking at what other people have done, and then lots of learning by doing (and failing). For what kind of language / mathematics do you want to write notations? Somebody might then be able to point you in a direction where somebody else wrote notations for something similar
This suggests that the need for a tutorial is very real...
Lutz Wrage (May 25 2021 at 12:47):Paolo Giarrusso said:
It also helps to understand how LL(1) parsing works, and the Camlp5 manual. You can't write an LL(1) grammar without understanding a bit on the implementation, and using Coq notations is no easier. After that, most things become much easier (tho I wouldn’t say “easy”).
I understand how LL(1) parsing works, so it's off to learning Camlp5, then. It seems there are various tutorials available. Any recommendations on a good one?
Paolo Giarrusso (May 26 2021 at 21:33):To clarify, I haven't "learned Campl5", but I've looked up SELF and NEXT in the Campl5 manual; I don't have a tutorial to recommend, because for the basics I've mostly followed examples in Coq IIRC :-|
It also depends on where you're getting stuck.
Paolo Giarrusso (May 26 2021 at 21:34):FWIW, this is a short summary (not a tutorial) re the left factoring problem https://gitlab.mpi-sws.org/iris/iris/-/blob/3cd45dbc6bf7b1a7e30990df6396401526848c37/docs/proof_guide.md#notations
Last updated: Oct 13 2024 at 01:02 UTC