yoshihiro503 OCaml/Coq/Scala @yoshihiro503@mstdn.jp

千葉県埼玉県から通うとすると東京の混雑する地域をまたいで毎日通勤することになる気がする。
関東の人は当たり前のことなのかな

新宿、渋谷、六本木にある会社ってあんまり子育て世帯向きじゃない気がする。
子供たくさんと東京で暮らすのは向いてないし、神奈川県は子育て支援制度があんまりないから。

もう少し頑張って証明のプルリク作るぞ！

ライブラリの導入とか環境構築はopamのあるCoqが断トツで強いと思う。
スレッジハンマーや自動証明のパワーはイザベル先生さすがといった感じ

特殊記号を多用するのは正直開発効率悪くしていると思う。

とりあえず then haveとusingを多用して問題を切り分けるスタイルを学んだぞ。autoとスレッジハンマーがとんでもなく便利だからあとは無理やりなんとかなるかも！？

英語キーボードしか触ったことない自分にとって日本語キーボードのマックは新鮮だった。
スペースの左が英数で右がかな。切り替えボタンが一種類じゃないの難しいね

イザベル難しいぞ！HOLだから楽勝かなと思ったけど、

電車も並ぶ、乗り換えも並ぶ、コンビニも並ぶ、それが東京

@yoshihiro503 一月を四週間とすると、週あたり4回以下の座れる電車通勤と、週あたり3回のぎゅうぎゅう電車通勤、どっちがいいかって話か。

税金やら手当やらを考えると、年収が上がっても手取りが下がることってあるよね

通勤時間自由で通勤で座れるけどリモート可の日が月当たり5回までの会社と、リモートは週二回OKだけど出社時間が決められている会社だとどっちが幸せなんだろうか

満員電車苦しい

数学バーというのに行ってみる

ocaml setup.ml -build

opam/opam の depends に次を追加

+ "re" { <= "1.6.1" }

Cannot load /home/mube/ocamltter/_opam/lib/re/re_perl.cmxs: cannot find file /home/mube/ocamltter/_opam/lib/re/re_perl.cmxs in search path

∗ install ppx_monadic 1.0.5 [required by ocamltter]
∗ install spotlib 3.1.2 [required by ocamltter]
∗ install ppx_orakuda 3.0.1 [required by ocamltter]
∗ install ppx_meta_conv 2.4.1 [required by ocamltter]
∗ install ocamltter 4.1.1*

∗ install re 1.9.0 [required by ppx_orakuda]
∗ install ppx_deriving 4.1.5 [required by ppx_meta_conv]
∗ install tiny_json 1.1.4 [required by ocamltter]
∗ install ppxx 1.3.0 [required by ppx_monadic, ppx_meta_conv, ppx_orakuda]
∗ install pcre 7.2.3 [required by ppx_orakuda]
∗ install base64 3.2.0 [required by ocamltter]
∗ install ppx_test 1.4.1 [required by spotlib]

∗ install zarith 1.7 [required by cryptokit]
∗ install seq 0.1 [required by re]
∗ install ppx_tools 5.0+4.03.0 [required by ppx_monadic, ppx_orakuda]
∗ install omake 0.9.8.7 [required by ocamltter]
∗ install base-bytes base [required by base64]
∗ install ocurl 0.8.2 [required by ocamltter]
∗ install cryptokit 1.13 [required by ocamltter]