2010-07-19から1日間の記事一覧
何かを定義する時に、 ∃n > 0.n + n > 0のように、0より大きなある自然数nを加算した結果は0よりも大きいという意味が無い命題を書きたい時に ∃n > 0といった、ある種自然数のsubtypeを作って定義を進めたい、というような時、Agda2ではどう書くのが良いんだ…
何かを定義する時に、 ∃n > 0.n + n > 0のように、0より大きなある自然数nを加算した結果は0よりも大きいという意味が無い命題を書きたい時に ∃n > 0といった、ある種自然数のsubtypeを作って定義を進めたい、というような時、Agda2ではどう書くのが良いんだ…