Prop
#Fleeting_Notes
Prop
命題
を表す型
命題宇宙、命題の
型宇宙
例:
$ P \land Q \rightarrow Q \land P : \text{Prop}
bool ≠ Prop
Propは「証明可能」か「証明不能」かの2つを表す
Propは
非可述的
(impredicative)
集合のように振る舞う命題？という
sProp
というのが他にある
LeanのProp
確認用
Q. Prop
関連
mere proposition
第一級市民
Sort 0
(Lean)
参考
Prop_J: 命題と根拠 | ソフトウェアの基礎
メモ
Doctrines | The n-Category Café
type of propositions in nLab
『Software Foundations Vol.1 Logical Foundations』
調査用
Google.icon
Prop(日)
Google.icon
Prop(英)
Wikipedia.icon
Prop - Wikipedia(日)
Prop(検索) - Wikipedia(日)
Wikipedia.icon
Prop - Wikipedia(英)
Prop(検索) - Wikipedia(英)