orange @[email protected]

なんか、Leanって結局は証明を書くことが主目的で、その主張に矛盾がないかを一応自動で検証してくれる環境であって、SMTソルバーみたいに推論してくれる環境ではないんだね・・・＞＜
目的外に使おうとすると、全部言われないとわからない呑み込みが悪い人的な環境＞＜；

「行間まで読んで取りうるすべての可能性を！！！　どう考えてもこうにしかならないだろゴルァ！」がSPARKで、
「どういうこと？」がLean？＞＜；

SPARKやDesign by Contractな環境が「こいつの説明に矛盾が無いか、説明しつくしていない部分が存在しないのかを全自動で完璧にガチガチに検証してくれる環境」であるとすると、
Lean 4は「こいつの説明に矛盾が無いか見てみる」程度であって、ぜんぜん推論してくれない感じ？＞＜；

ていうか、部分範囲型を作ろうとすると、整数と証明のタプルみたいなの（？）になるの、どういうことなの？＞＜；

Lean 4ちょっぴりいじってみたけど、SPARKとかと全然違いすぎてどういうことなのってなってる＞＜；
あまりにも思ってたんと違う＞＜；

Lean 4使えた＞＜（使えてない）

熊本地震で「Yahoo!天気」が意外な活躍？　断水・停電情報など投稿続出　ライフライン情報共有の場に（1/2 ページ） - ITmedia NEWS
https://www.itmedia.co.jp/news/article/2607/29/2000000277/

2023 グッドデザイン賞
八代市庁舎
https://www.g-mark.org/gallery/winners/15684

無いよりはマシとはいえ、階段の注意喚起の点字ブロック状構造物が床と同色なのはどういうことなの？＞＜；

八代市庁舎の免震構造が損傷　建て替えたばかり、工事では汚職事件も [熊本県] [2026年熊本地震]：朝日新聞
https://www.asahi.com/articles/ASV7Y34K4V7YTLVB00FM.html

八代市庁舎 | JIA日本建築大賞・優秀作品選 | 日本建築家協会 建築年鑑
https://jia-award.jia.or.jp/kenchikusen/2023/best-architecture/2055/

「メルマガは解除したけど、IDだけあっても何も起きないので気にしないならIDはそのまま放っておいておkだけど、もし解約したいのであればさらに返事ください」的に書いてあった＞＜

そういえば前に、なんかよくわからない会員向けメルマガが届き続けてて、「ずっとスルーしてたけど、そもそもこれって何だろう？＞＜；」と思い経って、
問い合わせ窓口に「メルマガ止めてほしいんですけど、そもそも全く記憶にないし何のサービスなのかすらさっぱりわかんないです＞＜」（＞＜以外ほぼ原文）って送ったら、「お調べしましたところ、元々は音楽制作ソフトウェア配布の××に入会され、それが△△に統合され、さらに当社のIDに統合されたという流れのようです」って返事来た事がある＞＜；

メアドかなんかの重複しか考慮してなさそうだけど、たぶん実際に統合作業するまで重複がどの程度かわかんないよね・・・＞＜

電子図書「道路橋示方書・同解説Ⅰ～Ⅴ」（令和７年改訂版）発刊のお知らせ
電子図書利用サービスについて｜公益社団法人　日本道路協会　Japan Road Association
https://www.road.or.jp/e-books/news_250930.html

"Ⅱ 鋼部材・鋼上部構造編：電子版 16,500円（紙版 18,260円）"

高い＞＜；

大石久和さんが、年頭所感で『淮南子』の中の「築土構木」が土木の語源であるという俗説を紹介しちゃった曰く付き(？)の号だ！＞＜；
数ヵ月後に、近年の俗説であってたぶん違うよってツッコミ記事が掲載された＞＜