Prop - pogi-log

Prop

#Fleeting_Notes

Prop

命題を表す型

$ P \land Q \rightarrow Q \land P : \text{Prop}

bool ≠ Prop

code:lean

#check And -- Prop → Prop → Prop

#check Or -- Prop → Prop → Prop

#check Not -- Prop → Prop

#check Implies -- Prop → Prop → Prop

variable (p q r : Prop)

#check And p q -- Prop

#check Or (And p q) r -- Prop

#check Implies (And p q) (And q p) -- Prop

確認用

Q. Prop

関連

sProp (集合)

メモ

Doctrines | The n-Category Café

調査用

Google.icon Prop(日)

Google.icon Prop(英)

Wikipedia.icon

Prop - Wikipedia(日)

Prop(検索) - Wikipedia(日)

Wikipedia.icon

Prop - Wikipedia(英)

Prop(検索) - Wikipedia(英)