MR ゆいれーる

なんか、そんなのを見つけてきた人が

　てだこ浦西から、空港まで

巨大ディスプレイ付き車両でいくらしい

いや、まぁ、まるで昔の LaserDisk Shooting みたいな。いや、なんか期待したわけではないんだが

ソニーの提供とかいってたが、ディスプレイって、もう作ってないんじゃないかな

そこそこ大きい。80inch くらい? 後ろが透けて見えるんだが、かなり綺麗だ

窓枠がないのはきれい

まぁ、そこになにを映すかは、沖縄のだめさがでるわけだけど

違うところの映像を出されると酔う

別に普通の短篇映画でいいんじゃないのと思わなくもなかったかな

Okica の半額モニタ

きました。まぁ、いいんだけど

　今使ってる Okica の番号

で、十分なはずだろ? 終わったら送り返せだのうるさい

果てしなきスカーレット

これは、名作じゃないですか? まぁ、嫌いな人もいると思うけど、それは

　心が汚れてるから

だろ? アベンジャーとかハリウッド系の残念な話に比べて、ぜんぜんいいじゃんん

デンマークとか王国とかの話も、まったく関係ない。最初のシーンで、あ、これは

　死んでからの話だと、はっきりわかる

昔のNHKの木星行きのロケットの中で目覚める話とか、コニーウィリスの航路とか、そういうジャンルの話なわけね

　スカーレットが強くて綺麗で可愛くて、いじめられる
　そして、目覚める

まぁ、あのお兄ちゃんどうなのとは思わなくもないけど。なんで日本人なんだよ

まあ、あんな能天気なのは、もはや日本人にしかいないような気もする

さいきん、ほうせんか観たので、「あれよりはぜんぜんいい」いや、あれだって、そこそこ面白かった

そういえば、あれも、なんか良いように見えなくもない男の話だった

https://scarlet-movie.jp/

lightening

ライカムのNewcommにいったら、Lightening / HDMI のケーブルが1980円なので、レジに持っていったら

　7980円です

はぁ? それならいらないです。Amazon で1980円で売ってるのに、なんで、そんな値段で買うのか

で、そのままコジマにいって、おっちゃんに聞いたら「Lightening cable はうちではもう扱ってない。Amazon で買え」

というわけで、プライムな奥様にお願いすることに

Apple TVがめねおけば良かったんだよな

VLC使ってみてもよいんだが

なんか、不便な世界だよな

NASと録画

まぁ、別にいいんだが、昔のまだ見てない録画が NAS に

　CCさくら、Gundam 00、レコンギスタ

くらいなんだが。ところが

　PS3/PS4 では観れなくなった
　NAS上のDLNAサーバはいまいち

まぁ、商売上の理由なんだろうけどね。アマプラでは有料

録画したBD出せば観れるんだが、せっかくNASに入っているのにね

でも、CIFS経由なら見る方法はいくらでもある。でもPCつなくの?

　MP4にencodeしなおせばPS3/PS4で観れる

いや、やらんだろ? 昔ならやったかも

Lightening cable / HDMI 変換で見る、Apple TV経由で見るとか

なんだかね〜 まぁ、Lightneng cable / HDMI は2千円しないから…

Lean 4

Agda と同じ定理証明系なんですが、少し触ってみようかと

VSCode で入れるらしいが、入るけど

　　なに入力すればいいの?

まぁ、ChatGTPに聞けばいいか。#eval 1 + 2 とかするらしい

import First.Basic

#eval 1 + 2

def square (x : Nat) : Nat :=
x * x

#eval square 4

theorem hello1 : 1 + 1 = 2 := by
decide


コマンドラインからできるんだろと思ったが、なんか、動かない

+leo+kono ~/.elan/bin/lean First.lean
First.lean:3:0: error: unknown module prefix 'First'
No directory 'First' or file 'First.olean' in the search path entries:


build は動く

+leo+kono ~/.elan/bin/lake build -v First.lean
ℹ [2/3] Replayed First.Basic
trace: .> LEAN_PATH=/Users/kono/src/lean/test1/First/.lake/build/lib/lean /Users/kono/.elan/toolchains/leanprover--lean4---v4.25.2/bin/lean /Users/kono/src/lean/test1/First/First/Basic.lean -o /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First/Basic.olean -i /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First/Basic.ilean -c /Users/kono/src/lean/test1/First/.lake/build/ir/First/Basic.c --setup /Users/kono/src/lean/test1/First/.lake/build/ir/First/Basic.setup.json --json
ℹ [3/3] Replayed First
trace: .> LEAN_PATH=/Users/kono/src/lean/test1/First/.lake/build/lib/lean /Users/kono/.elan/toolchains/leanprover--lean4---v4.25.2/bin/lean /Users/kono/src/lean/test1/First/First.lean -o /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First.olean -i /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First.ilean -c /Users/kono/src/lean/test1/First/.lake/build/ir/First.c --setup /Users/kono/src/lean/test1/First/.lake/build/ir/First.setup.json --json
info: First.lean:5:0: 3
info: First.lean:10:0: 16
Build completed successfully (3 jobs).

なんか、結構、えげつない呼び出しだな

まぁ、動いたみたい。

一旦、C に変換するの? 微妙だな

agda みたいに「全部、Haskell でがんばる」ってのがいいかどうかは、また別だけどね

Restrant Lily

沢岻の少し奥にあるレストラン

経塚のサンエーから、あるいて330までいく途中で見かけました

行ってみたい気もする

崖崩れする前にいった方がよいか?