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

この動画見てたら、すごく小さいときに牛乳瓶の蓋に切れ込みを入れて輪ゴムを使って飛ばして遊んでたのを思いだした。

https://www.youtube.com/watch?v=rI5iUSuyoYA

さいあく F-84W が私に似合ってなかったとしても薄いから服の下に隠せばいいんだ。半袖だと無理だけど。

スマホのアラーム使えばいいじゃんとかそういうのあるけど、結局あれは色んな通知とかがまざるしよくまれに充電切れる(充電しろ)し信頼できない。やはり腕時計がいいのだ。

外出時に時報をオフにして帰宅時に時報をオンにする習慣を付ければいい。行動科学を以ってすればこの程度造作もない(雑に言ってる)。

昔はアラームが5つあるモデルも買ったことあるんだけど、あれは結局使いこなせなかった。結局アラームは一個でいいんだ。どうせ目覚しは腕時計に期待することじゃないわけで、1つのアラームを状況に合わせて使いこなせればそれでよい。

外でちょっと時報がなっちゃったときの迷惑レベルはそこまでじゃないと思う。一瞬、「ピ！」ってなっちゃうくらいのことは許されて欲しい。

何に期待して F-84W をまた使おうとしているのかというと、時報機能。生活において時報は地味に役立つ機能だと思う。まあ、外出時に鳴らないように細心の注意が必要だが家での生活においてなんか便利だと思う。

G-SHOCK も買ったんだけどあれはちょっとゴツすぎるし、操作も複雑でつらい。シンプルな方がいい。

色々考えた結果、腕時計は CASIO の F-84W を使うことにした。なんか似合ってないとか言われることもあるけど気にしない気にしない。

なんとなくソフトウェアのプロジェクトページを作ってみた。

Pict-conshttps://www.tojo.tokyo/projects/pict-cons.html

Emacs のテーマ、意外とデフォルトのテーマって結構良いのではないかと最近思うようになった。

暦の計算で役立つ以外になんかあったんだろうか。

昔の日本の謎の数学ムーブメントなんだったんだろう。西洋と違ってあんまり実用的な話じゃない感じだし本当にただ「解けた！」「やった！」という感じでしかないのが面白い。

あ、これブラウザの話か。自分への影響はなさげだけどよくない話ではあるな……。

現実的に考えると GNU Guile よりも Racket の方がインストールしやすいので、とりあえず vikalpa を Racket に移植する感じになるかな。マクロには syntax-case 使ってるしたぶん簡単だと思ってる。

J-Bob よりもインターフェースが優れてると思うので、定理証明手習いの障壁が下がると思うんだよな。

次は自分で作った定理証明支援系である vikalpa の動画投稿しようかな。ただあれはコードがごちゃごちゃしてるところあるし、リファクタリングしたい気持ちあるんだよな。

動画作る大変さって本当にやってみないと分からないものだと思う。得にエンコードがつらい。だいぶ fps と画質を犠牲にした。

新記事投稿しました。解説動画付き記事という試み。

自動定理証明器 ACL2 の入門向けに L-99 の1問目を解きましたhttps://www.tojo.tokyo/acl2-L-99-1.html

Windows にはメモ帳っていう優れたアプリケーションがあるんだからそれ使えばいいのになんでわざわざ Word で情報をやりとりするんだろう。