Where is a good place to learn Ltac2?
I wish there were more examples in the Coq documentation
This topic was moved here from #Coq users > Ltac2 learning resources by Karl Palmskog.
this was mentioned in a similar thread: https://github.com/coq/coq/tree/master/test-suite/ltac2
There's also https://github.com/tchajed/ltac2-tutorial, not sure how up-to-date it is though
Last updated: May 31 2023 at 04:01 UTC