高階論理でも型を構成したいときって、あるよね

Isabelle/HOLにsubset typeないかな〜と思って「Isabelle/HOL subset type」とか「Isabelle/HOL comprehension」とかで調べていましたが、全然見つからず、最終的にtypedefがその役割を担っていることが分かりました。これがあれば集合から型を作れるので、便利です。

Isabelle/HOLには他にもquotient typeがあるのですが、これはeffectiveでしょうか、そうではないのでしょうか。いずれ確認しましょう。今から楽しみですね。

この記事は個人サイトでも読めます。