よく使う Coq.Logic の公理 - 簡潔なQ
Coq.Logic にはCoqの集合論モデルにおいて正しい公理や、それらの間の関係が記述されている。 ここではその一部を取り上げて、意味を説明する。 前提知識 公理を仮定しない状態では、 Coqの論理は直観主義論理である。 ある2つが「等しい」という命題が証明できる場合は限定される。 証明の文脈(Prop)における「AまたはB」と、値の文脈(Set/Type)における「AまたはB」は区別される。前者から情報を取り出すことはできないようになっている(マッチングの型検査で弾かれる。) 以下、公理の説明 古典論理 (classical logic) 場所: Coq.Logic.Classical 古典論理で証明できることは、例えば以下の内容がある。 排中律 ( P or not P ) 二重否定除去および背理法 ( if not not P, then P ) 決定性の値の取り出し (descr
〇〇の常識は■■の非常識
This ticket describes an issue where operations on a Data.Map in Haskell version 6.13.20100801 can produce invalid trees. Specifically, applying deleteMin twice to a map produced by fromList results in a tree that valid? returns false for. The ticket includes a code sample demonstrating the problem. It also notes that valid? returning false indicates the tree is in an invalid state.Read less
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
