技術と魚

雑感と備忘録

2021-05-26から1日間の記事一覧

Coq再入門 - SetとProp

Coqにおける Set, Prop は(型の型(=種類)的な意味で) sort という。ともにbuilt-in Setはプログラムやデータ型のためにある Propは証明や命題のためにある # Set Prop アトミックな項 Program, データ Proof 証明 型 Specification, データ型 Proposition 命…