Q @masterq@pawoo.net

調理時間を半分にしたいです、、、 https://pawoo.net/media/KgxKU3Tg2J0FmhLfM7w

やはりCoqはツラいという感触を得つつあります、、、

あかん。。。"wlog:/"がさっぱりわからない。。。

コアーションややこしい。。。

そうか。。。タクティクそのものは停止することが保証されていないのか。。。

スペースによるインデントで良かったのでは、、、使いこむとまた違う感想を持つのでしょうか。。。

"-case"とか"+case"とかの符号って実質インデント扱いなんですか。。。

なんとー / "PlatformIO IDE for VSCode — PlatformIO 3.6.0 documentation" http://docs.platformio.org/en/latest/ide/vscode.html

ちゅーんさんはポインタの宣言をHaskellで書いてプリントすればいいんじゃないかと思いました。 http://hackage.haskell.org/package/language-c / "ちゅーん vs くいなちゃん ポインタ解ってる - Togetter" https://togetter.com/li/262116

"by"が可読性を向上させることが理解できました。なるほど

"rewrite /=." さんバージョンによって挙動が変化したりしないのでしょうか。。。

こんなの延々証明しなきゃじゃないか。。。 #add2n

addn1とか全部覚えなきゃなんですか。。。

いまいちしっくりこないけれど
1 subgoal
X, Y : Prop
XtoY_is_true : X -> Y
X_is_true : X
______________________________________(1/1)
Y
というコンテキストから
MP
: forall X Y : Prop, (X -> Y) -> X -> Y
が作られると理解しました。

なんで
Theorem MP : Y.
が
MP
: forall X Y : Prop, (X -> Y) -> X -> Y
になるんだ。。。

素人にはmove使いやすそう。。。

日本語うれしい。

doneじゃなんでダメだったんだろうか。。。

"by []." 謎な記述方式ですね。。。 #Coq #SSReflect

hatsugaiさんが重要なことをコメントに書いている。。。