2023.06.30
https://www.youtube.com/watch?v=bGEkVdFrilo
知った
観た
たすけてー!& 本当に何?で面白かった
思った
Lean 4のtermination_byとdecresasing_byは理屈はわかっているんだけどもどうやって証明すれば良いのかの具体例が少なすぎて全然わからない 知った
"I'd like to thank all those who made this night necessary."
「今晩(の授賞式)を出席せざるを得ないものにしてくださった皆様に感謝いたします」
"those who made this night possible"(今晩の授賞式を実現してくださった皆様)と言うべき所でpossibleをnecessaryに言い誤ったもの。
「皆様のお蔭で今晩の授賞式がある」と感謝するはずが、「皆様のせいで今晩の授賞式に出席しなければならない羽目となった」という、迷惑がるような意味になってしまっている。