Wordle 344 5/6
🟨⬜⬜⬜⬜
⬜🟨🟨⬜⬜
⬜🟩⬜⬜🟨
🟩⬜🟨⬜⬜
🟩🟩🟩🟩🟩
あの歌のあれだが
posted at 06:45:24
Stats | Twitter歴 6,198日(2007/04/10より) |
ツイート数 225,853(36.4件/日) |
表示するツイート :
Wordle 344 5/6
🟨⬜⬜⬜⬜
⬜🟨🟨⬜⬜
⬜🟩⬜⬜🟨
🟩⬜🟨⬜⬜
🟩🟩🟩🟩🟩
あの歌のあれだが
posted at 06:45:24
母音が多くてもやさしいとは限らないのか
三つ目でもう少しがんばって当てられたはず
posted at 06:50:39
MtG 用語なの?
posted at 06:58:59
英語に関しては入試で英検準一級相当を要求するのが明解。必須にすればやると思われる。東アジア圏でも大学入試の規準としては割と普通。
それくらいでないと英語の授業についていけない。英語での授業を可能にすると講師の幅が大きく広がる。
posted at 07:04:16
まぁ、ありそう。わざわざ練習する必要があるとは思わないかな。
QT 避難所の子どもに飲ませるものが水しかなく、その時に水を飲み慣れていない子が脱水症状になるケースが何件かあった
posted at 07:07:22
日本語も、あんまりちゃんと足切りできてないかも。
もっとも翁長先生が入試の国語の配点を大きくしたら数学のできない学生ばかりになって工学部のうちでは困ったことになったってのはあった。
posted at 07:09:36
入試の英語、どうも準一級レベルにするのに反対してる感じがあってな〜
どういうことなんだよ
と詰問したい。その程度を教えることのできない英語教師ってなんなんだよ。
posted at 07:16:18
英検準一級は高校在学中に受けるべき。(と昔の自分に言いたい
posted at 07:16:33
Agdaでの商集合はわりとめんどくさい
準同型定理書いてみるか
posted at 07:41:58
まぁ、彼女のことだからわざとだな。
posted at 07:52:52
RawGroup と Group の違いってなんだ?
posted at 08:17:46
rawMonoid は field じゃないのか。だったら、RawGroup は Group じゃないじゃん。
posted at 08:22:11
そうそう、逆なんだよ。部分群は準同型写像で定義する。
posted at 08:40:01
Y 頻繁に使っていたので、neovim で Y がないのは痛いな。
定義すれば良いんだが...
posted at 08:54:11
正規部分群まで書けた
posted at 09:09:15
一応、Yに関する議論はあるみたいだな。
https://github.com/neovim/neovim/issues/416…
posted at 09:43:47
しばらく使ったけど、emacs / viper の方が
neovim / agda-vim よりかましか
直せば良いんだが...
posted at 10:27:16
でも、長く英語使ってるから、無駄に語彙力は増えてる
wordle とか。
posted at 10:28:32
macOS の spell correction が
spaceを打つ時に
勝手にはずれなものに変換する
のは致命的。おせっかいとかのレベルじゃなくて気が狂ってる。
posted at 10:31:02
普通に disable だが、check はして欲しいんだよな。
頭のおかしいのをなおさないってのがなぁ。
posted at 10:33:49
@ForestLine2 ですよね…
その辺り評価されないから
やらないよね
posted at 11:32:45
お、準同型定理書けた
posted at 11:57:29
やっぱり、neovim agda 実用にならんな
posted at 12:11:03
やっぱり準同型定理ってのは普遍問題の解なの?
posted at 12:16:55
商群書いてる。めんどくさい。
posted at 12:31:33
@shima__shima MBP入れ替えるまでは切ってたんですが
入れてみようかと思った僕が馬鹿でした
posted at 12:39:32
特に問題なく消滅できそう
排中律関係はまだ不明
posted at 12:40:14
商群が細かい。でも、それだけで出そうだな。
後で普遍問題の解に帰着させるのもできるんじゃないか説
posted at 13:43:10
なにせ、Ace combat と FF13 挫折中なので、もはや、コンソールゲームはいいかなという気分。
posted at 14:28:06
水を飲めない子供たち
原始は安全な水とかなかったので果物とから水を取ってたのかも。水をそのまま飲む方が異常でさ。
今みたいにくそ甘い果実じゃないんだよな。そこで水を飲むのを強制するのは残念な感じもある。
posted at 15:28:00
どっちかというと金稼いできてるのは営業だ的な人たちが多かった気がする。そういう人たちは格が低いのはそうだな。
posted at 15:31:34
むしろ技術に詳しい、あるいは開発に近い人が営業もするパターンもある。
posted at 15:31:45
技術関係の人は営業苦手なのであって、別に格が低いとかは考えてない。そもそも営業が重要なのは上位の戦略が悪いか、競争が厳しいところをわざわざ選んでるかだが…
posted at 15:34:40
なんか agda-vim 動かなくなった
posted at 15:40:05
f x ・f y は、f (x ・y)なんだが、行き先がどこかはよくわからない。
posted at 16:19:16
商群はこれで良いが全部書くのはそこそこ大変
あとは準同型定理のhを作れば良い
posted at 17:48:00
あれ、なんか、準同型定理、refl なんだけど。
どーして
まぁ、なくはないんだが…
posted at 18:08:05
h 作る時に kernel 使ってないが…
posted at 18:11:39
準同型定理は値に関しては自明なので、まぁ、良いのかも。(いや、ないだろ)
posted at 18:16:55
普通にhが普遍問題の解だってのがわかる
posted at 18:40:31
いや refl でいいのかな
posted at 19:22:48
全体的な構成は合ってるが、商群とhの構成にへくってるっぽい。たぶん、G/Kの代わりにGを作ってしまってるんだろうな。それなら refl になる。
posted at 22:33:45
kernel 使ってないし
posted at 22:37:13
基本的にはToposの時と同じにKernelを作ってるのだが、だいぶ違う。排他律使わないし。
posted at 22:38:12