ほとんど終わりました。ほとんどは、brew/brew cask で。
ちょっと、はまったのは、Agda のlibraryの設定。blog に書き忘れたんですが、Agda に自分のlibraryを付け加えるには、
＊ ~/.agda/libraries
/usr/local/Cellar/agda/2.5.2/lib/agda/standard-library.agda-lib
/Users/kono/src/public/category-agda/category-agda.agda-lib
＊ ~/.agda/defaults
standard-library
category-agda
というのを書く必要があるのでした。Emacs 側からできるのかも知れないけど、まぁ、いいや。
brew list
＊ agda cabal-install gdbm mercurial openssl python sqlite
＊ antiword emacs ghc nkf pkg-config readline
brew cask list
＊ emacs mactex pdftotext
ぐらいですね。
Papers3 も、~/Documents/Papers3 をcopyして、Paper.appをいれて、ライセンス指定して終わり。
mhは、どうも、nmh ではなく MH-JPを使っているっぽいな。なんだよ。
Friday, 30 June 2017
Wednesday, 28 June 2017
新しいMBP
EnPITの予算関係でもらえるらしく。EnPIT ありがとうございます。学部でやってくれっていうのも、通って嬉しいです。
今のMBP、結構、引き継ぎ引き継ぎで来たので、さすがに clean install でいこうかなと。ほとんどのファイルはサーバ上にあるので、無理に手元におかなくてもよいかな。
つうか、このまま移行すると、ラズパイのimageとかあるので、かなり時間かかるはず。670GBも使ってるな。
というわけで、つまり、あんまり移行できてません... Ansible とか Docker みたいなので minimum install したい...
iCould にデータを全部移すかみたいなのが出てくるけど、ちょっと高いのがな。1TBなくすとか、また、せこいわざを...
File Vault とかもデフォルトで入れようとするようですが、 もちろん拒否。
無意味なセキュリティのおかげで、OS X上のOSの課題がめんどくなっているのがいくつか... dtrace とか gdb とか。
Unix系は、だいたい brew で入れられるはず。
Xcode
X11
TeX
Agda (Emacs/Haskell)
X11のAgda用のfont
hg
perl/Tk
nmh
ラズパイ用のqemu
Virtual Box
VMWare fusion
Papers3
FreeMind
Omni Graffle
Google Photo Backup
QuickRes (なんか有料になっていた...
滅多に使わない LibreOffice
あとは自前のPerl script 群か。Dockerも入れたんだが、ほとんど使ってない。
Google Drive も、もっと積極的に使って良いのかも知れんが、あんまり、気が進まなくてなぁ。
今のMBP、結構、引き継ぎ引き継ぎで来たので、さすがに clean install でいこうかなと。ほとんどのファイルはサーバ上にあるので、無理に手元におかなくてもよいかな。
つうか、このまま移行すると、ラズパイのimageとかあるので、かなり時間かかるはず。670GBも使ってるな。
というわけで、つまり、あんまり移行できてません... Ansible とか Docker みたいなので minimum install したい...
iCould にデータを全部移すかみたいなのが出てくるけど、ちょっと高いのがな。1TBなくすとか、また、せこいわざを...
File Vault とかもデフォルトで入れようとするようですが、 もちろん拒否。
無意味なセキュリティのおかげで、OS X上のOSの課題がめんどくなっているのがいくつか... dtrace とか gdb とか。
Unix系は、だいたい brew で入れられるはず。
Xcode
X11
TeX
Agda (Emacs/Haskell)
X11のAgda用のfont
hg
perl/Tk
nmh
ラズパイ用のqemu
Virtual Box
VMWare fusion
Papers3
FreeMind
Omni Graffle
Google Photo Backup
QuickRes (なんか有料になっていた...
滅多に使わない LibreOffice
あとは自前のPerl script 群か。Dockerも入れたんだが、ほとんど使ってない。
Google Drive も、もっと積極的に使って良いのかも知れんが、あんまり、気が進まなくてなぁ。
Monday, 26 June 2017
フードフリー and 黒ガー
日曜日は、いつもの宜野湾のフードフリー。なんですが、
割とすいてました
なんでかな。宣伝不足? 良くあるのは宣伝担当者が変わったとかかな。
で、真夜中に Ingress Guardian が150日に。1月辺りにも139までいったのがあったんですが、屋富祖だったので、最近activeになった緑(gurukamaとかfound000とか)にやられました。
1月に青の作戦があったんですが、
http://seeker-s-eye.blogspot.jp/2017/01/okinawa-ingress-resistance-operation.html
その時の反転ポータルの処理のやつみたいです。真夜中にあんなところに取りに行ったのか。
この所、沖縄は緑優勢。宜野湾真栄原も「網羅的に焼く」人が何人か。いや、僕もいろんなところを網羅的に焼きにいくわけですが。なので、真栄原辺りだとガーポは厳しいかな。
もっとも、ご近所指向の僕が取れるくらいなので、沖縄のIngressのactivity自体が結構落ちているってことだろうな。
割とすいてました
なんでかな。宣伝不足? 良くあるのは宣伝担当者が変わったとかかな。
で、真夜中に Ingress Guardian が150日に。1月辺りにも139までいったのがあったんですが、屋富祖だったので、最近activeになった緑(gurukamaとかfound000とか)にやられました。
1月に青の作戦があったんですが、
http://seeker-s-eye.blogspot.jp/2017/01/okinawa-ingress-resistance-operation.html
その時の反転ポータルの処理のやつみたいです。真夜中にあんなところに取りに行ったのか。
この所、沖縄は緑優勢。宜野湾真栄原も「網羅的に焼く」人が何人か。いや、僕もいろんなところを網羅的に焼きにいくわけですが。なので、真栄原辺りだとガーポは厳しいかな。
もっとも、ご近所指向の僕が取れるくらいなので、沖縄のIngressのactivity自体が結構落ちているってことだろうな。
Tuesday, 20 June 2017
Sunday, 18 June 2017
小澤の不確定性原理
昨日のOSCの飲み会でビール飲みまくっていたら「先生どこですか」的な呼び出しが研究室OBから。なんで沖縄戻ってきてるのと聞いたら、
＊ 科学基礎論学会/科学哲学/科学史
＊ http://phsc.jp/conference.html
ぐ、懐かしすぎる。ぜんぜんアンテナに引っかかってませんでしたが、琉大でやってるのか! で、プログラムを見ると、
＊ 出口弘
＊ 小澤正直
ぐ、懐かしすぎる。東工大の吉田夏彦先生配下な人たちではないですか。
なんですが、さすがに三日連チャンで早起きは無理でした。遅刻しつつ、小澤さんの発表を聞くことができました。
＊ σ(P)σ(Q) + ε(P)σ(Q) +ε(P)ε(Q) > hoge
だったかな。Hiesenberg のドイツ語の論文のアブストラクトとかが出てるのが吉田研っぽくって面白かったです。不確定性は indeterminancy から来ているのだけど、元のドイツ語は inaccuracy に相当する言葉だったらしい。それを英語の共著者が inderminancy とまずい訳をしたと。それにEinsteinが引っかかって、あんな議論になったかと思うと、まぁ、そんなことはないと思いますが。あの議論は量子力学の定義の精密化には訳なったわけだし。
というわけで、懐かしい面子に会えて良かったです。
＊ 科学基礎論学会/科学哲学/科学史
＊ http://phsc.jp/conference.html
ぐ、懐かしすぎる。ぜんぜんアンテナに引っかかってませんでしたが、琉大でやってるのか! で、プログラムを見ると、
＊ 出口弘
＊ 小澤正直
ぐ、懐かしすぎる。東工大の吉田夏彦先生配下な人たちではないですか。
なんですが、さすがに三日連チャンで早起きは無理でした。遅刻しつつ、小澤さんの発表を聞くことができました。
＊ σ(P)σ(Q) + ε(P)σ(Q) +ε(P)ε(Q) > hoge
だったかな。Hiesenberg のドイツ語の論文のアブストラクトとかが出てるのが吉田研っぽくって面白かったです。不確定性は indeterminancy から来ているのだけど、元のドイツ語は inaccuracy に相当する言葉だったらしい。それを英語の共著者が inderminancy とまずい訳をしたと。それにEinsteinが引っかかって、あんな議論になったかと思うと、まぁ、そんなことはないと思いますが。あの議論は量子力学の定義の精密化には訳なったわけだし。
というわけで、懐かしい面子に会えて良かったです。
Saturday, 17 June 2017
OSC Okinawa 2017
いつもの内輪の展示会ですね。そういえば、両親も業界の内輪の展示会では暇そうにしていたっけ。
展示はいつものなんですが、セミナーのネタがなくて。なので、
＊ 2月にいじっていた cmake の入門をやろう
と思ったわけですが、聴衆は自分の学生以外は三人でした。ま、まぁ、地味な話だからな。
cmake は、mavenとかgradleとかに近いかな。make が、わりと魔境になってしまっているので、
add_target ( target_name source1.c source2.c )
だけで、いい感じにやってくれるのは便利。まぁ、そこからいろいろやろうとすると、どうせ魔境なんだけど。
今回は自治会館。コンベンションセンタ、あるいは、OISTよりは、はるかに便利なところ。特に今日は雨だったので、沖縄では珍しい「駅から濡れずにいける会場」なのはうれしい。
展示はいつものなんですが、セミナーのネタがなくて。なので、
＊ 2月にいじっていた cmake の入門をやろう
と思ったわけですが、聴衆は自分の学生以外は三人でした。ま、まぁ、地味な話だからな。
cmake は、mavenとかgradleとかに近いかな。make が、わりと魔境になってしまっているので、
add_target ( target_name source1.c source2.c )
だけで、いい感じにやってくれるのは便利。まぁ、そこからいろいろやろうとすると、どうせ魔境なんだけど。
今回は自治会館。コンベンションセンタ、あるいは、OISTよりは、はるかに便利なところ。特に今日は雨だったので、沖縄では珍しい「駅から濡れずにいける会場」なのはうれしい。
Friday, 16 June 2017
GPU VDM
https://groups.oist.jp/external-events/event/gpu-accelerated-vdi-international-conference-2017-asia
いや、まぁ、琉大にはGPUクラスタないし。システム更新でも「GPUは毎年新しいのが出るから」で見送られたりしたので、いや、だったら、毎年なんか買えよ〜
と言うわけで、少し場違いなわけですが、まぁ、全然関係ないわけでもないしなぁ。今年の2月ぐらいはMac ProのGPUと格闘してたし。というわけで、プレゼンもすることに...
OISTなので、学生に車で送ってもらうわけですが、
8時と言ったのに、ぜんぜん来ない
間に合わないよ、で、かなに「すみません、送ってください」と頼んで階段を降りたら、下から登ってくるうちの学生が。「道が混んでて8時に出たのに30分かかりました」って、いや、そこ「8時に迎えに来て」って言ったのが「8時に迎えに出る」になっているところが、沖縄なんだよな。
まぁ、僕も、そんな感じで、いまだに遅刻魔なわけですが。
そこそこお金取られたので、ちょっと厳しい。学生の分がな。
そして、明日は OSC Okinawa です。そっちも、よろしく。一応、うちの学生のcmakeのセミナーもあります。というわけで、学生にはいろいろ迷惑かけてます。
いや、まぁ、琉大にはGPUクラスタないし。システム更新でも「GPUは毎年新しいのが出るから」で見送られたりしたので、いや、だったら、毎年なんか買えよ〜
と言うわけで、少し場違いなわけですが、まぁ、全然関係ないわけでもないしなぁ。今年の2月ぐらいはMac ProのGPUと格闘してたし。というわけで、プレゼンもすることに...
OISTなので、学生に車で送ってもらうわけですが、
8時と言ったのに、ぜんぜん来ない
間に合わないよ、で、かなに「すみません、送ってください」と頼んで階段を降りたら、下から登ってくるうちの学生が。「道が混んでて8時に出たのに30分かかりました」って、いや、そこ「8時に迎えに来て」って言ったのが「8時に迎えに出る」になっているところが、沖縄なんだよな。
まぁ、僕も、そんな感じで、いまだに遅刻魔なわけですが。
そこそこお金取られたので、ちょっと厳しい。学生の分がな。
そして、明日は OSC Okinawa です。そっちも、よろしく。一応、うちの学生のcmakeのセミナーもあります。というわけで、学生にはいろいろ迷惑かけてます。
Tuesday, 13 June 2017
Prolog とシーケント代数
去年も今頃授業でやっていたみたいです。関数型言語と同じで、
＊ プログラム中での変数の論理的関係が理解しやすいように記述する
ための指針みたいなものだと思うと良いと思う。Prolog 使うとバグがなくなるとか、そんなことではなくてさ。
Prolog のbaseになっているシーケント代数の方もやるんですが、自然演繹と両方やるのはちょっとなぁ。まぁ、たいした量じゃないから両方かな。
でも別にシーケント代数やっていたら、Prolog 理解しやすくなるというわけでもなく。でも、Prolog で使う範囲だと推論規則が少なくて良いってのはあるかな。
Σ |- Q, Γ Σ' , Q |- Γ'
---------------------------------------------------------- (cut rule)
Σ , Σ ' |- Γ , Γ'
これだけだものな。
実際のProlog programmingだと多用(つうか濫用)するのは単一化の方なので、単一化を詳細にやらないのはどうなのとも思うのですが、やろうと思うと結構煩雑。
Clausal form への変換のプログラムも少し探してみたんですが、結構、複雑で、授業で紹介するにはどうなのかな。確か、Clockskin and Merish の教科書にも変換プログラム載っていたと思うんだけど、割と大変だった。
アセンブラのマニュアルとかは「ちょっと論理式かプログラムで書いてくれ」と思うことはあります。
＊ プログラム中での変数の論理的関係が理解しやすいように記述する
ための指針みたいなものだと思うと良いと思う。Prolog 使うとバグがなくなるとか、そんなことではなくてさ。
Prolog のbaseになっているシーケント代数の方もやるんですが、自然演繹と両方やるのはちょっとなぁ。まぁ、たいした量じゃないから両方かな。
でも別にシーケント代数やっていたら、Prolog 理解しやすくなるというわけでもなく。でも、Prolog で使う範囲だと推論規則が少なくて良いってのはあるかな。
Σ |- Q, Γ Σ' , Q |- Γ'
---------------------------------------------------------- (cut rule)
Σ , Σ ' |- Γ , Γ'
これだけだものな。
実際のProlog programmingだと多用(つうか濫用)するのは単一化の方なので、単一化を詳細にやらないのはどうなのとも思うのですが、やろうと思うと結構煩雑。
Clausal form への変換のプログラムも少し探してみたんですが、結構、複雑で、授業で紹介するにはどうなのかな。確か、Clockskin and Merish の教科書にも変換プログラム載っていたと思うんだけど、割と大変だった。
アセンブラのマニュアルとかは「ちょっと論理式かプログラムで書いてくれ」と思うことはあります。
Sunday, 11 June 2017
メッセージ
観てきました。原題が Arrival で、元の小説のタイトルは「あなたの人生の物語」ですね。
元の短篇が割と何も起きないタイプの話で地味。で、その通りに極めて地味に始まって「どーすんのこれ」だったのですが、ハリウッド的な拡大解釈が入っていて、そこそこ盛り上がりました。よろしかったです。
こういう、どうしようもなく人類が変わってしまう話って割と好きかも知れないな。正解するカドとか。
異世界言語の学習という視点ではどうなんだろう。深層学習使うシーンとか欲しかった気もするけど。一応、データの視覚化はやってたか。
アメリカ人的には、異星人がテレビとかラジオから英語勉強して、いきなり流暢な英語を話すとかを期待してるのかな。この手の言語習得は18-19世紀にはたくさんあったはずなので、そのあたりの蓄積があるはずなんだけどね。今はもう需要はないのか。
元の短篇が割と何も起きないタイプの話で地味。で、その通りに極めて地味に始まって「どーすんのこれ」だったのですが、ハリウッド的な拡大解釈が入っていて、そこそこ盛り上がりました。よろしかったです。
こういう、どうしようもなく人類が変わってしまう話って割と好きかも知れないな。正解するカドとか。
異世界言語の学習という視点ではどうなんだろう。深層学習使うシーンとか欲しかった気もするけど。一応、データの視覚化はやってたか。
アメリカ人的には、異星人がテレビとかラジオから英語勉強して、いきなり流暢な英語を話すとかを期待してるのかな。この手の言語習得は18-19世紀にはたくさんあったはずなので、そのあたりの蓄積があるはずなんだけどね。今はもう需要はないのか。
Friday, 9 June 2017
Emacs 25 の続き
というわけで、Emacs 25 と Agda 2.5.2 は、xterm/Terminal.app 上では完全に壊れてしまって。C-C C-L するたびに→が増殖する始末。気持ちはわかる。Emacs は昔の端末流に描画の最適化ってのをやるわけ。この位置だけ書き換えればよい的な。それを、Unicode 上でやると、どうしても位置がずれる。Terminal 上での描画幅は正確には知り得ないから。でも、行頭から順に描画すれば良いはず。なので、vim とか Emacs 22 では問題ない。壊したのがいるってことね。
しょうがないので、GUI版を試してみようと思うわけですが、どうinstallするのかが謎。結論的には Mac OS X では、Homebrew で、
とすれば良いらしい。また、Emacs 入れ替えか。
Agda 側は
brew install agda
で良いらしいです。Haskell は brew install ghc らしい。
で、GUIで立ち上がるわけですが、
Font が小さい
いや、 2880x1778 で k14 使っている僕が言うんだから、かなり小さい。文字幅1mmないだろ。でも、Agda は動いているっぽい。
で、Emacs の文字の大きさを変える旅に出るわけです。
C-X C-+
で一時的に大きくなるのはすぐにわかりました。そして、Option Menyu に Set Default Font... がある。大きくして、Set Default Font か。
もちろん、再起動で元に戻る
あ、あーん? で、見つけたページがこれ。
Emacs：一発で文字サイズを変更する方法
http://lioon.net/emacs-change-font-size-quickly
つまり。「GUIから文字サイズを変える手段はない」ということらしい。.emacs か! そこで、
Set Default Font... を押すと Font Menu は出てる
というのには気がつきました。でも意味はないらしい。 Set Default Font... ってのは嘘ってことね。Font Menu は閉じないと再起動でも開く。なんだよ。
なんですが、このページに書いてある通りにしても動かない。Twitter でぐちっていたら、
.emacs があると、.emacs.d/init.el は読まないよ
って、ばっちりそれでした。mv ~/.emacs ~/.emcas.d/init.el か。
それで動いたんですが、翌朝になるとまた動かない。なんだよ〜
そのうち、
fontset-standard undefined
とか言われて、New window もできないように。
で、init.el の中で frame の font を指定してみたら、
VL Gothinc not found
とか言ってる。そうか、
そのままコピペしたのがだめなんだな。VL Gothinc を monaco に変えたら動きました。あ〜 疲れた。
vim 版の Agda を試してみるべきだな。
しょうがないので、GUI版を試してみようと思うわけですが、どうinstallするのかが謎。結論的には Mac OS X では、Homebrew で、
brew tap caskroom/cask
brew cask install emacs
とすれば良いらしい。また、Emacs 入れ替えか。
Agda 側は
brew install agda
で良いらしいです。Haskell は brew install ghc らしい。
で、GUIで立ち上がるわけですが、
Font が小さい
いや、 2880x1778 で k14 使っている僕が言うんだから、かなり小さい。文字幅1mmないだろ。でも、Agda は動いているっぽい。
で、Emacs の文字の大きさを変える旅に出るわけです。
C-X C-+
で一時的に大きくなるのはすぐにわかりました。そして、Option Menyu に Set Default Font... がある。大きくして、Set Default Font か。
もちろん、再起動で元に戻る
あ、あーん? で、見つけたページがこれ。
Emacs：一発で文字サイズを変更する方法
http://lioon.net/emacs-change-font-size-quickly
つまり。「GUIから文字サイズを変える手段はない」ということらしい。.emacs か! そこで、
Set Default Font... を押すと Font Menu は出てる
というのには気がつきました。でも意味はないらしい。 Set Default Font... ってのは嘘ってことね。Font Menu は閉じないと再起動でも開く。なんだよ。
なんですが、このページに書いてある通りにしても動かない。Twitter でぐちっていたら、
.emacs があると、.emacs.d/init.el は読まないよ
って、ばっちりそれでした。mv ~/.emacs ~/.emcas.d/init.el か。
それで動いたんですが、翌朝になるとまた動かない。なんだよ〜
そのうち、
fontset-standard undefined
とか言われて、New window もできないように。
で、init.el の中で frame の font を指定してみたら、
VL Gothinc not found
とか言ってる。そうか、
(set-fontset-font "fontset-standard"
'ascii
(font-spec :family "VL Gothic" :size 20) nil 'prepend) ;; ここでサイズを指定
(set-fontset-font "fontset-standard"
'japanese-jisx0213.2004-1
(font-spec :family "VL Gothic") nil 'prepend)
(setq default-frame-alist
(append (list
'(font . "fontset-standard"))
default-frame-alist))
そのままコピペしたのがだめなんだな。VL Gothinc を monaco に変えたら動きました。あ〜 疲れた。
vim 版の Agda を試してみるべきだな。
Thursday, 8 June 2017
新しい Agda
Sets (集合を対象、写像を射とする圏)の Completeness としばらく格闘していたんですが... Compleness ってのは Limit があることで、Limit ってのは、与えられた関手で示された対象と射のグラフ上の可換関係を代表する対象みたいなものらしい。
直積とかは二つの要素の代表なんだけど、それがあれば、その二つの要素にできることは全部できるじゃないですか。そんな感じ。
なんだが、なかなかできなくて。結局、
という record を作れば Limit の uniquness 以外は簡単に示せました。なのだが、uniquness が堅い。要するに、field 二つが等しければ、record 自体が等しいという合同性の問題らしい。
でも、ググってたら、にたようなのを Stack Over Flow で見つけました。(良くある)
https://stackoverflow.com/questions/37488098/equality-on-dependent-record-types
なのだが、こいつの例題が通らない。もしかして、Agda の version の問題か? 確かにちょっと古いんだよな。
で、update をかけたんですが... なんか、emacs も update。あ、てめーちょっと待て。
emacs 25 に上げられてしまったおかげで、xterm 上の色とかUTF8がずれまくる。vim は大丈夫なんだけど。くそ、unusable だ。しかも。Agda は 25 でないと動かない。
GUIでしか動かさないあほが手を入れて xterm 側を壊してるんだよな。
で、肝心の例題は Agda のupdate で通ったんですが、Sets completeness の方は通らず。くそ〜 どうも問題は Agda のrecord の合同性の扱いそのものにあるっぽい。僕のせいじゃないらしいです。
が通るはず。だけど、通らない。これはあきらめた方が良さそう。
なので、Agda 壊れちゃったので、ちょっと困ってます。vim で編集して emacs でチェックみたいな感じ。
直積とかは二つの要素の代表なんだけど、それがあれば、その二つの要素にできることは全部できるじゃないですか。そんな感じ。
なんだが、なかなかできなくて。結局、
record snat { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ )
( smap : { i j : OC } → (f : I ) → sobj i → sobj j ) : Set c₂ where
field
snmap : ( i : OC ) → sobj i
sncommute : ( i j : OC ) → ( f : I ) → smap f ( snmap i ) ≡ snmap j
smap0 : { i j : OC } → (f : I ) → sobj i → sobj j
smap0 {i} {j} f x = smap f x
という record を作れば Limit の uniquness 以外は簡単に示せました。なのだが、uniquness が堅い。要するに、field 二つが等しければ、record 自体が等しいという合同性の問題らしい。
でも、ググってたら、にたようなのを Stack Over Flow で見つけました。(良くある)
https://stackoverflow.com/questions/37488098/equality-on-dependent-record-types
なのだが、こいつの例題が通らない。もしかして、Agda の version の問題か? 確かにちょっと古いんだよな。
で、update をかけたんですが... なんか、emacs も update。あ、てめーちょっと待て。
emacs 25 に上げられてしまったおかげで、xterm 上の色とかUTF8がずれまくる。vim は大丈夫なんだけど。くそ、unusable だ。しかも。Agda は 25 でないと動かない。
GUIでしか動かさないあほが手を入れて xterm 側を壊してるんだよな。
で、肝心の例題は Agda のupdate で通ったんですが、Sets completeness の方は通らず。くそ〜 どうも問題は Agda のrecord の合同性の扱いそのものにあるっぽい。僕のせいじゃないらしいです。
snat-cong : { c : Level } { I OC : Set c } { SObj : OC → Set c } { SMap : { i j : OC } → (f : I )→ SObj i → SObj j }
( s t : snat SObj SMap )
→ ( ( λ i → snmap s i ) ≡ ( λ i → snmap t i ) )
→ ( ( λ i j f → smap0 s f ( snmap s i ) ≡ snmap s j ) ≡ ( ( λ i j f → smap0 t f ( snmap t i ) ≡ snmap t j ) ) )
→ s ≡ t
snat-cong s t refl refl = refl
が通るはず。だけど、通らない。これはあきらめた方が良さそう。
なので、Agda 壊れちゃったので、ちょっと困ってます。vim で編集して emacs でチェックみたいな感じ。
Friday, 2 June 2017
iPhone 7
このあいだ、また、iPhone の画面を割ってしまって。ワイシャツのポケットがほつれれてでかいiPhoneだと落ちやすい。落ちどころが悪いとわれるらしいです。
で、5月で2年しばりが消えるので、ソフトバンクからは抜けようと思っていたのでちょうど良かったんですが、MNPとか面倒くさすぎる。かなのauの家族割に入るのがやすいらしいが...
まあ、格安SIM試してみるんじゃないの?
っことで、IIJ MIO に。めんどくさいけど、ソフトバンクにで電話して、うだうだ話してMNP予約番号をもらう。こんなのWebから一発発行でいいのに。IIJの方はWebから申込。で、iPhone 7 plus は Apple から買うと。はい終わり。
と思ったが、IIJの認証が通らない。免許証の写真を upload する方式なのだが、そもそも普段使いのクレカでは通らないとかわけわからん。で、サポートに電話したんですが、
コーノとコウノ
の違いだったらしい。いや、コーノで統一しているんだが、通らないあほシステムが若干あって、そこではコウノにするしかない。ローマ字側を kouno で強制するのとかも見たことがあります。もしかすると、免許証がそれだったかも。
免許証には漢字しかない
はずので、おかしな話ではあるな。
と言うわけで、ネックはIIJ側だったらしい。SIMがくれば、
iPhone を最新iOSでバックアップ
SIMをactivateして、新しいiPoneのOSを最新に
そこに restore
という手順で動いたみたいです。まぁ、しばらくいろいろあるだろうな。
で、5月で2年しばりが消えるので、ソフトバンクからは抜けようと思っていたのでちょうど良かったんですが、MNPとか面倒くさすぎる。かなのauの家族割に入るのがやすいらしいが...
まあ、格安SIM試してみるんじゃないの?
っことで、IIJ MIO に。めんどくさいけど、ソフトバンクにで電話して、うだうだ話してMNP予約番号をもらう。こんなのWebから一発発行でいいのに。IIJの方はWebから申込。で、iPhone 7 plus は Apple から買うと。はい終わり。
と思ったが、IIJの認証が通らない。免許証の写真を upload する方式なのだが、そもそも普段使いのクレカでは通らないとかわけわからん。で、サポートに電話したんですが、
コーノとコウノ
の違いだったらしい。いや、コーノで統一しているんだが、通らないあほシステムが若干あって、そこではコウノにするしかない。ローマ字側を kouno で強制するのとかも見たことがあります。もしかすると、免許証がそれだったかも。
免許証には漢字しかない
はずので、おかしな話ではあるな。
と言うわけで、ネックはIIJ側だったらしい。SIMがくれば、
iPhone を最新iOSでバックアップ
SIMをactivateして、新しいiPoneのOSを最新に
そこに restore
という手順で動いたみたいです。まぁ、しばらくいろいろあるだろうな。
Subscribe to:
Posts (Atom)