2005-05-29 [長年日記]
λ. 永夜抄スペカ取得率: 214/222/222
久し振りに東方永夜抄をプレイ。Lunaticを頑張ってノーコンテニュークリア。7機で始めてクリア時に残機0・ボム0という惨状だけどね。で、Lunatic 6Bのスペルカードを中心に何枚か回収したので、取得済み/挑戦可能/総数 が 214/222/222 になった。残るは以下の8個。取れそうな気がするのは「ライフスプリングインフィニティ」と「永夜返し -丑の四つ-」くらいか……
- 禁薬「蓬莱の薬」 (Lunatic)
- 神宝「ライフスプリングインフィニティ」 (Lunatic)
- 神宝「蓬莱の玉の枝 -夢色の郷-」 (Lunatic)
- 「永夜返し -丑の四つ-」
- 「インペリシャブルシューティング」
- 「エンシェントデューパー」
- 「夢想天生」
- 「深弾幕結界 -夢幻泡影-」
ところで、「永夜返し -子の四つ-」は「子の刻」「子の二つ」「子の三つ」よりも簡単な気がする。
λ. Extensional Equality in Intensional Type Theory. Thorsten Altenkirch
を読んだ。問題意識は良くわかるのだけど、モデルの構成がイマイチよく分からなかった。
(2005-09-17 追記) 読み返したらあらかた理解できた。けど、まだ幾つか理解できていない概念がある。large elimination とか。
(2005-09-30 追記) Agdaでも実装してみた。An Implementation of a setoid model in Agda.
(2006-05-30 追記) large elimination は多分 elimination した結果が要素ではなく集合などになるような elimination 。
hardもクリア出来ない俺だがエンシェントデューパー、夢想天生は取ったきがするよ。
いやいや、オレにクリアできてjnセソセイにクリアできないなんて、ぶっちゃけ有り得ないから。7機で始めれば絶対クリア出来るって。<br><br>夢想天生は頑張ってパターンを作ればいけそうとは思う。エンシェントデューパーはタイミングを合わせられなくてムリポ。
エンシェントデューパーはすぐとれるよ、多分。<br>この中でもとくに難易度低いし。<br>夢想天生は一度とれるようになると簡単だよ。
エンシェントデューパー、実は百回以上挑戦してたり……(汗