トップ «前の日記(2005-05-28) 最新 次の日記(2005-05-30)» 月表示 編集

日々の流転


2005-05-29 [長年日記]

λ. 永夜抄スペカ取得率: 214/222/222

久し振りに東方永夜抄をプレイ。Lunaticを頑張ってノーコンテニュークリア。7機で始めてクリア時に残機0・ボム0という惨状だけどね。で、Lunatic 6Bのスペルカードを中心に何枚か回収したので、取得済み/挑戦可能/総数 が 214/222/222 になった。残るは以下の8個。取れそうな気がするのは「ライフスプリングインフィニティ」と「永夜返し -丑の四つ-」くらいか……

  • 禁薬「蓬莱の薬」 (Lunatic)
  • 神宝「ライフスプリングインフィニティ」 (Lunatic)
  • 神宝「蓬莱の玉の枝 -夢色の郷-」 (Lunatic)
  • 「永夜返し -丑の四つ-」
  • 「インペリシャブルシューティング」
  • 「エンシェントデューパー」
  • 「夢想天生」
  • 「深弾幕結界 -夢幻泡影-」

ところで、「永夜返し -子の四つ-」は「子の刻」「子の二つ」「子の三つ」よりも簡単な気がする。

Tags: 東方

λ. 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 。

本日のツッコミ(全4件) [ツッコミを入れる]
ψ jn (2005-05-31 06:44)

hardもクリア出来ない俺だがエンシェントデューパー、夢想天生は取ったきがするよ。

ψ さかい (2005-06-01 00:14)

いやいや、オレにクリアできてjnセソセイにクリアできないなんて、ぶっちゃけ有り得ないから。7機で始めれば絶対クリア出来るって。<br><br>夢想天生は頑張ってパターンを作ればいけそうとは思う。エンシェントデューパーはタイミングを合わせられなくてムリポ。

ψ wisteria (2005-06-02 16:34)

エンシェントデューパーはすぐとれるよ、多分。<br>この中でもとくに難易度低いし。<br>夢想天生は一度とれるようになると簡単だよ。

ψ さかい (2005-06-06 23:45)

エンシェントデューパー、実は百回以上挑戦してたり……(汗