Hacker News Reader

Comment by 082349872349872 | Hacker News Reader

A cursory search reveals they're not builtin, but were written for the talk: https://github.com/awalterschulze/ccc-talk/blob/main/Coq/src...

    nail ~= intros
    wat ~= discriminate
    etc.

"wreck" is actually "destruct", "same" is "reflexivity"...

It boggles the mind why the author would make up fanciful new names for the fundamental tactics in this "how to" article.

He's giving a talk, it's for the lulz

If you are giving a talk on a theorem proving programing language you're gonna want to make it fun

The only useful ltac I see in there is compare, which can save a lot of tedious rewrites, when needing that frequently.