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

Lean 4 のチュートリアルとして Theorem Proving in Lean 4 を読んで練習問題を解いたりしているのだけど分かりやすい気がする。練習問題を解くのはパズルみたいで結構楽しい。

つらそうなパターンっぽくてつらい。バイナリを入れる Guix のパッケージ定義を書く方法学ぶか。。。
https://github.com/leanprover/lean4/issues/6392

Lean が面白いぞというメールが届き気になってる。とりあえずインストールだけしてみようと思う。

1, 2, 3 ... までしか分からないから、初項1公差1の等差数列とは限らないのか。

ビスケットが0枚のときにもポケットを叩くとビスケットが1枚になるなら自然か。まあ、不思議な話なので気にしても仕方がない。

ポケットを叩いた効果が、今入っている全部のビスケットに影響するはずなので、+1 されるのは変なんだよな。

そもそもなんでふしぎなポケットのことを考えているのか

ポケットにビスケットを入れた段階では、まだ叩いていないから 2^0 でビスケットの数は1枚。

編集履歴
n^2 → 2^n → 2^(n-1) → 2^n
はあ、疲れてる。。。

ふしぎなポケットのビスケットが増える歌、叩くたびにビスケットの数が +1 されるのに違和感がある。叩くたびに ×2 されていって叩いた数 n に対してビスケットの数が n^2 になる方が自然に感じる。

趣味プログラミングとして、Typed Racket でLuhnアルゴリズムを実装したのでそのことについて記事を書きました。
Typed Racket を使ってなにか書いたのは久しぶりだったのですが、いい感じに型がついてよかったのでしばらくは Typed Racket で何かをして記事を書くというのをやっていこうと思います。

Typed RacketでLuhnアルゴリムを実装した
https://www.tojo.tokyo/posts/typed-racket-luhn.html

私のメール、特定の条件を満たすものを自動的にお気に入りするみたいな設定をしているっぽくて、メールのお気に入りだらけになっていて真のお気に入りと区別不可能であることに気づいたため設定直さなきゃ。

カナル型イヤホン怖いな。カナル型じゃない良い感じのBluetoothイヤホンを後で探そう。今持ってる百均で買ったカナル型のやつが意外に便利で結構長期間使うようになったので。

リノートされてからの言及を見に行かない限り気づけないので厄介。見にいかなきゃよかったと思ったことある。

なんか、リッチデザインのときの方が匠による至高の作品みたいなこだわりが伝わってきてよかったんだよな。

企業ロゴはホームページのファビコンになったりするだろうしなあ。

立体感のあるリアリティの高い画像をアイコンにすると縮小・拡大に弱くなって厳しいということか。ぼやけるとか以前に小さくなると細かいところがよく分からなくなるし仕方ないのか。。。

デザインの流行の変化を感じるやつだ。私は立体感があるのが好きなのだけど、最近はフラットデザインとかマテリアルデザインとかいって平面的なのが多くなった。

混乱してる。unstage は git restore --staged なのか。

git restore と git reset と git add で分けて作業しないといけないのは面倒くさそうだな