3 ms·

"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 t

"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.

21eleven 3y ago
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