Notices by きゅーけー (tojoqk@mastodon.tojo.tokyo), page 257

makibo でも良さそうと思ったけど、英語配列とUSB接続がなさそうなのがなー

うーん、一刻も早く欲しいわけではないし、一般販売が始まったときにも欲しかったら買うのでいいかな。

Makuake｜タッチパッドとマウス機能を キー表面で操作可能にした 革新的キーボード｜マクアケhttps://www.makuake.com/project/prestigio_click_and_touch/

これはキーボードとトラックパッドの自動切り替えを使いこなすのに技能が必要な可能性があるけどそれでも欲しいな。悩んでる。

メモリとスワップがめっちゃ逼迫してた。定期再起動するか。

サーバーが重そうなので再起動してくる

早朝にスーパーへ行って食材を手に入れたので久しぶりに自炊してる

やはり職場の Slack で共有する勇気はない。際どい内容だな。

仕事に戻らないと

NHK プラスでもみれるっぽい。https://plus.nhk.jp/watch/st/e1_2021011817049

https://www.nhk.or.jp/meicho/famousbook/105_sihonron/index.html

明日の早朝と深夜に再放送があるっぽい

2021年1月20日（水）午前5時30分～5時55分／Eテレ2021年1月20日（水）午後0時00分～0時25分／Eテレ

受信料で NHK オンデマンド使わせて欲しいのめっちゃ分かる。

NHKオンデマンド | １００分ｄｅ名著 マルクス“資本論”　（３）「イノベーションが“クソどうでもいい仕事”を生む！？」https://www.nhk-ondemand.jp/goods/G2020111595SA000/

これはよかった。NHK の存在意義を強く実感する回だったな。

あと5分が永遠に続けばいいのに

今日は朝早くスーパーへ行ったのでお昼は自炊する。営業日連続自前記録が断たれた。

ACL2 の日本語情報がほぼないので使えるようになって ACL2 を広めたい。

手動で何度か証明したことによって少し証明探索機の気持ちが分かるようになったかもしれない。これで一度挫折した ACL2 を使いこなせるかも。

まだドキュメントはないので使い方を把握するのは困難な状況なのですが、下記で append の結合性の証明をしているのでなんとなく何をやっているのかは把握できるかもと思ってます。

https://gitlab.com/tojoqk/vikalpa/-/blob/f5879492135a41edd1f227607dcbc8d0c25c5c3c/tests/test-vikalpa.scm#L346

Guile で動く定理証明支援系を作った。だいたい自分の望むものは手に入ったので、とりあえずはこれを使って『定理証明手習い』を一周してみようと思う。

https://gitlab.com/tojoqk/vikalpa

起きた