Tutorial Ltac2 for Ltac1 users#131
Conversation
thomas-lamiaux
force-pushed
the
tuto-Ltac2forLtac1
branch
from
7a968f6 to
e31882b
Compare
Durbatuluk1701
left a comment
Durbatuluk1701
left a comment
There was a problem hiding this comment.
Sorry if I was overly pedantic, just excited to have high quality Ltac2 docs. I think it looks great, thanks for undertaking the task!
agontard
left a comment
agontard
left a comment
There was a problem hiding this comment.
Hi, thank you for this tutorial! It felt indeed like a nice introduction.
Here are some comments I have (note that perhaps some differences are due to compiling with Rocq 9.1).
Apologies for the amount, I tried to exhaustively list everything I noticed/didn't understand.
@agontard Don't worry, as long as they are useful it is good to report them. |
| hypothesis named [id] regardless of what was passed. | ||
|
|
||
| To pass Ltac1 values across this boundary, one uses the binder syntax | ||
| [ltac2:(x1 .. xn |- expr)], which explicitly receives Ltac1 values as Ltac2 |
There was a problem hiding this comment.
It was unclear which Ltac1 values it would receive/how. This change would clarify it for me:
"explicitly receives Ltac1 values as Ltac2" -> "explicitly receives the Ltac1 values x1 .. xn as Ltac2"
|
|
||
| but is lacking a notation enabling us to directly write [clearbody x y] to | ||
| clear the body of the local definitions [x] and [y]. | ||
| This problem will be solved over time with contributions to the standard library. |
There was a problem hiding this comment.
This is a political question, it is not clear that we want to add such notations.
|
@SkySkimmer as the Ltac2 expert is the content correct ? |
6 participants
Uh oh!
There was an error while loading. Please reload this page.