時の庭2

なんか、前に閉めてた時の庭、普天間のカフェ、ラーメン金川のそばですが、店主が変わって復活してました

前と違って、食べ物がたくさんある。それは良い

でも、ボロネーゼに生卵のせるのはやめて

Wifi も電源もそのままなので、使いやすい。長続きすると良いんですけど

OSC Okinawa 2025

Sakuraのいつもの場所で。なんか、

　00年代と参加者が変わってない感じ

でも、そのまま人は歳くってる感じね

シス管の琉大生が一人。高校生がブース持ってたな

さむい〜

沖縄、20度きるとかなり寒くて

チョッキを出してもらいました

　「このソファをちょっとどけて出せるところにあります」

いや、それ無理だから…

図南の翼

なんとなく読み返してしまう本

十二国記の一冊だけど、珠晶が12歳で、王を目指して登極する話ね

NHKのアニメではやらなかった

話に無理がないわけではない。というか無理の塊

でも、なんか読み返したくなる

玉泉洞

本土からお客さんとしか来ないわけですが

なんか、年何ミリとか成長するらしく

床が既に鍾乳石化してる

入ったのは20年ぶり? 900m は結構長い

そして、その後のお土産公園が長い

鍾乳石の先が白くなってる。ここ20年分の成分の変化かな。二酸化炭素で白くなるのかな?

Okica はわかりました

Okica のポイントのサイトを見たら、

　月4万円で20%還元

になってる。あぁ、それだと1万円還元はあるな

いったい、いつ、1%から変更になったのか?

Prince concert on IMAX

なんか、ふっと調べたら、浦添パルコで11/20まで。一週間だけか。まあ、80年代だろ? おじいちゃんおばあちゃん用?

仕方ないなで観に行ったんですが

　Led Zeppelinの時の只券は使えない

え〜 しかも、特別上映で3千円。見てるのは、3人

いいけどさ。Prince って、まぁ、お祭りバンドなんだよな。なので楽しかったです。シーラE が良い

なんだが

　　一曲も知ってる曲がなかった

どういうことなんですかね。聞いてたのは90年くらいのはずなんだが、このコンサートは1987なんだよな

なんとなく、Electric Miles っぽい

Prince はヒゲが嫌いな人は多いかも?! 没後10年?!

https://towapictures.co.jp/prince_sign-o-the-times/

月と龍

大平のラミロワールの向かいにあると聞いたのでいってみました。 2022にオープンしたらく。

お昼にいったが作りが料亭。断られるかと思ったが入れて

　お昼は、2,600円からの魚の御前

あぁ、まぁ、やられた感じはあるが、そんなものか

個室に案内してくれたんですが、明かりが

　まるで事務室

な蛍光灯で、ちょっと料理が可哀想な感じ。魚はカンパチですが、まぁ、おいしかったです

値段相応

新しい nvim-agda

まぁ、動いてはいるんですけどね

なんか、知らんけど

　引数がずれる

goal 表示する時に、隣のを表示してしまうんだな。まぁ、害はない

前に使っていたのは「sub windowが出て表示する方式」だったんだが、こっちは「Windowを割って表示する」

まぁ、どっちでも。あと、term が表示が少し変。まあ、それも害はない

自分で作って使うと「そういうの気にならない」ところがあってさ、まぁ、そうなんでしょう

正気な人は VSCode を使っているんだろうとは思うんだけど

Lean は VSCode only らしい

自分の手元のを Lean に書き換えようって気もなくはないんですけどね

https://github.com/isovector/cornelis.git

首里城再建

なんか、もう儀保駅から見える -

公園の修理

330愛知のまつぼっくり公園の裏の通り、元浦添総合病院のところの330の上の通り

だいぶ前の台風でやられて閉鎖されてたんですが、最近、修理完了してるのを発見しました

地味に便利。Ingress にね

月を詠むのカレー

最近、通っているかも

昔は嘉数のソウエイシャっていう茶店をやってたらしい。短かったけどね

このカレーは南インド風? メニューが

　このカレープレートと、コーヒーとチャイ

くらいしかない。潔い。どうせ、いつも同じもの頼むので、それでよい

https://www.instagram.com/tsukiwo_yomu/

原神の紙芝居

月の関連のストーリーをやってるんだが

　途中で寝落ちすると、かなり前まで戻される

　わけわからん双六みたいなモード

ちょっとひどすぎない?

わざとか? まぁ、そろそろゲーム的に寿命なような気はする

かけ算の話 5m/s x 2kg =2m/s x 5kg

もともとの掛順は

(一つの皿に飴5つ分)x(皿2つ分) 5x2
(一つの皿に飴2つ分)x(皿5つ分) 2x5

で、「どっちでもいいだろ」だったはずだ。「だから、一つ分の差だろ」ってわけね

運動量の自然な累加の交換則

　5m/s x 2kg =2m/s x 5kg

は、
　2kg = (基準の量 1kg ひとつ分) x (2つ分) で2倍 　5m/s x 2kg = 5kg m/s x 2
　5kg = (基準の量 1kg ひとつ分) x (5つ分) で5倍 　2m/s x 5kg = 2kg m/s x 5

で、皿と飴の掛順と、まったく同じ構造を持ってる

　5m/s x 2kg =2m/s x 5kg の左右は2kgと5kgの差がある。これが掛順

この動かぬ掛順の証拠を「見ないふりして」話をそらすだけなのが反順序ならしい

結局、これだけで掛順の説明としては十分ならしい

「順序じゃなくて単位を無視するな。 5m/s x 2kg =2kg x 5m/s だから掛順はない!」

という反順序もいるんだが「まったく関係ない式」だよね? これは

　交換しない交換則
　「a x b = b x a の両辺は、aをb回足す」
というトンデモらしい。かけ算は「a x b はaをb回足す」という意味なのだから、交換しない交換則は
一階述語論理に対する反則みたいなものだ。もともと、そういう曖昧さを避けるために記号論理が開発されてるわけね

正しくは
　「a x b = b x a は、aをb回足すのと、bをa回足すのと値は等しい」
というわけ。これが掛順の説明にもなっている

まぁ、掛順を理解してるなら「かけ算の順序はどっちでもいい」のだが

　「かけ算に定義はない」
　「教科書のかけ算は定義ではない」
　「かけ算は累加ではない」
　「(ひとつ分)x(いくつ分)と(いくつ分)x(ひとつ分)の両方がある」
　交換しない交換則「PV=VPだから掛順はない」

これらは単なるトンデモ。教科書を読んで勉強しなおそう。今からでも遅くはないよ

https://x.com/shinji_kono/status/1895764620629197140

色褪せたポスト

沖縄の日差しだからな

昔の丸いのも嫌いでないけど、さっさとこれになってた

年金関連の書類が郵便なんだよな

まぁ、物理的所在を見たいのかもしれないけど、もっとましな方法あるだろとも思う

Neovim package manager

Lazy での設定は、ほぼ終わって、agda も動くようになったんですが、

　vim.pack.add()

ってのが次期 package manager になるってな話が

せっかくだから、試してみるか? なんだが、

　pack is nil

ってなんだ? 0.11 ではまだ入ってないらしい

　 NVIM v0.12.0-dev-1569+g16c8152229-Homebrew　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
で、試すと動く。なのだが、

　　"neovimhaskell/nvim-hs.vim" ,
　　"isovector/cornelis",

は、対応してない。これらは Haskell base だから。あっそ

まぁ、Lazy でいいか

nvim update の続き

.vimrc を init.lua に書き換えるだけだが、

^M ではなく <CR> と書くのか

vim.cmd とか vim.opt とか書けば良いだけ

package management には lazy ってのを使う

~/.config/nvim/init.lua
~/.local/share/nvim/lazy/

置き場所がよくわかんないんだが、まぁ、動いているらしい

設定は config に書いて、package は local にいく感じ? lazy が面倒見てくれるらしい

githun copilot も lazy 経由で

と思ったら、node.js が古いだと? v21 で、今は v25 か

次は autoload を書かないと

問題は、新しい agda vim UI が、微妙なところ

今ままで使ってるのは、若干、バグがあるんだが、自分でなおすのは既にめんどくさい

長い物に巻かれるのは嫌いじゃないんだが

homebrew updgrade

AgdaのSheafの方もだいぶ進んで、って

　まだやってるのかよ

て感じなんですけどね。でも随伴函手のηとεの定義まではできた

ところが、εの定義を接続すると Agda が止まらない。なので、

　そろそろ version up するか

と brew upgrade するわけだな

で、まぁ、いろいろ trouble が

　Perl/Tk の build に失敗する。って、ソースは5年前?!

他のものを探すと、Prima ってのがあるらしい。それは Aqua もあるらしいが、install してみたら

　X11 base

まぁ、それなら、Perl/Tkか。JPEG/jpeg を見直すと、system のlibjpegを使う設定の認識にしくってたのでそれでなおりました

ChatGPTがこの辺には便利

でも、agdaの方は

/Users/kono/src/CategoryExercise/src/@@HOMEBREW_CELLAR@@/ghc/9.12.2/lib/ghc-9.12.2/bin/./ghc-9.12.2: No such file or directory /opt/homebrew/bin/ghc: line 10: exec:

なんだこれ? 要するに、テンプレートからの生成に失敗しているらしい

結局、brew uninstall ghc ; brew insatall ghc で解決

ところが、nvim のplugin がトラブる。まぁ、予想はしてたんだが。ついでに

　　新しい plug in 試してみるか

で、https://github.com/agda/cornelis これを見るんだが

　　neovim では、init.lua で初期化するのが普通

って、いつからだよ。まぁ、neovim 使うってのは、そういうことだから、仕方ない

というわけで、emacs で止まらないことは確認したが、nvim では、まだ、動いてません

落書き

しちゃいけないところに書くから面白いわけで「落書きするな」では効果がない

割と良く見るサインの意味はなんだろ?