2021-02-12
前に来る複数の型に依存して次の型を決定するみたいな処理が必要だけど、TypeScriptでそんなの書けるのか？ 複雑さに比較して構文上のノイズをどれだけ削減できるのかみたいな問題もある
結合オペレータのAPIとして提供するだけならそこまで大変じゃなさそうだなあ
ffmpegでフルパワーでエンコードしたときに放熱が追いつかなくてサーマルスロットリングする ビルド回してるときは気付かなかったのでAVX2使うとダメとかそのへんかな Scrapbox、$ \LaTeX記法が正しいとき青に、間違っているとき赤になるようになってて便利だ ただちょっと青が暗くて見にくいので明るくした
これを「ウィクロス」と呼ぶのはだいぶ無理があるだろ
敵のみなさん、こんな運だけの奴らに負けても暴れないの偉い。人格が良すぎる
3話
運だけじゃなくなった！
EDの入りが完璧すぎるだろ
証明は大変だけど、やはり演習はやったほうがいいな
導出パートと同じ
やればやるだけ学びがある
学生を謳歌しているという感じがある、いいな
定理2.4-2.9までやった
2.9がかなりしんどい、補題が
2段の導出木のための条件を引き出すために和の交換法則と結合法則を駆使する
数字を並べてたらひらめいたけど、ひらめかなかったら地獄だったな
2.10も大変そう。2.11は量は多いけどそこまでではなさそう
自然数に対する帰納法が終わると次は算術式に対する帰納法が始まる
とはいえ、分岐が増えるだけでやることは変わらない
パターンマッチのケースを書いていくつもりでやればいい
最初はどう解くべきなのか全くわからなかったが、本に書かれている証明を見て「やっていい操作」を把握しつつ進めていったら何となくフレームワーク的なものがつかめてきて、複雑な証明も書けるようになってきた
条件に初期値を入れて制約を得て、その制約を求めたい判断に入れて示す
条件を考えて導出木を少し戻って規則から1つ戻った判断を導き、証明に必要な変数を得る
導いた判断を使って帰納法の仮定にあてはめて、さらに(有用な)判断を得る
必要に応じて判断を定理を使って加工して、求めたい判断の導出木に入れてQED