Agda の parameter と index の区別、フォーマルにはよくわかってない

∷ (U+2237) と ::（コロン (U+003A) 2 つ）の区別がつかずに詰まっていた

やっぱり Emacs に戻ろうかな……いまはもう Gemini 君いるから Emacs LISP もなんとかなりそうだし……

inductive type わからね～

実績解除：高輪ゲートウェイ駅に降り立つ

あと Gem というやつで「コーディングパートナー」というのがあって、こっちのほうがコーディングに強いのかなと思ってしばらく使ってたけど、なんかポンコツだな……と思ってやめたら、ふつうの Gemini のほうが賢かった

でも Zed でも頑張って拡張機能を書けば診断を表示させることはできるらしいので今度書いてもらおう。Gemini に。

Gemini に 4～5 時間教えてもらい、ようやく Agda の LSP が Zed で動いたものの、型ホバーは出るが診断は出ないという悲しい結果になった

コードについての LLM の正確性はすごいなあ。コード書けないまま人生を終えそう。

また生活がハチャメチャになってきた