オレンジはそれをわかってる上でアメ車が好き＞＜；
GMのサターンって、結局なんでアメ車が日本車に負けたのか全く理解していない人が作ったクルマと言えそうだし、たぶん今もアメリカ人は理解してなさそう＞＜
なぜならばアメリカの消費者はそんな事あんまり気にしないから＞＜；
日本がバブル期のころにアメリカで開発されて、日本に入ってきた時はむしろぴったり総崩れのタイミングかも＞＜
バブルではなくない・・・？＞＜
サターン (自動車) - Wikipedia
https://ja.wikipedia.org/wiki/%E3%82%B5%E3%82%BF%E3%83%BC%E3%83%B3_(%E8%87%AA%E5%8B%95%E8%BB%8A)
”日本へは1997年（平成9年）に進出。「礼をつくす会社、礼をつくすクルマ」というキャッチコピーで広告展開し、...”
orange
さんがブースト
あぁ……
サターンってバブル期に参入だったのか
バブル崩壊後の90年代でも販売は続いてたような記憶があるけど、全然売れてなかったよねぇ……
景気後退後も"輸入車=特別なクルマ"という構図は崩れなかった
同じ系統のクライスラー ネオン然り
まあ、後に参入したヒョンデ(当時はヒュンダイ)と起亜も日本市場に低価格な"普通のクルマ"の居場所はないと判断して撤退しましたね
根本的に日本市場における普通のクルマって国産9メーカー(当時)で間に合ってましたし……
それがBEVの登場で風穴が空いた、そこに目をつけて中国メーカーかヒョンデが日本に続々と進出している
というのが2026年現在の情勢ですかね
なんか、Leanって結局は証明を書くことが主目的で、その主張に矛盾がないかを一応自動で検証してくれる環境であって、SMTソルバーみたいに推論してくれる環境ではないんだね・・・＞＜
目的外に使おうとすると、全部言われないとわからない呑み込みが悪い人的な環境＞＜；
「行間まで読んで取りうるすべての可能性を！！！ どう考えてもこうにしかならないだろゴルァ！」がSPARKで、
「どういうこと？」がLean？＞＜；
SPARKやDesign by Contractな環境が「こいつの説明に矛盾が無いか、説明しつくしていない部分が存在しないのかを全自動で完璧にガチガチに検証してくれる環境」であるとすると、
Lean 4は「こいつの説明に矛盾が無いか見てみる」程度であって、ぜんぜん推論してくれない感じ？＞＜；
ていうか、部分範囲型を作ろうとすると、整数と証明のタプルみたいなの（？）になるの、どういうことなの？＞＜；
Lean 4ちょっぴりいじってみたけど、SPARKとかと全然違いすぎてどういうことなのってなってる＞＜；
あまりにも思ってたんと違う＞＜；
- ＠orange_in_space
2017年 4月に登録
