I used Coq in one class in school, and I never encountered wat or wreck. It’s possible they’re user- or library-defined tactics. One thing I think is important

I used Coq in one class in school, and I never encountered wat or wreck. It’s possible they’re user- or library-defined tactics. One thing I think is important about Coq is that it really is meant to be interactive. Even after a fair amount of usage I still find it somewhat tricky to just read a proof, especially a nontrivial one. A good IDE will show you a panel that includes all your hypothesis and requirements so far, updating as you run each line