高階論理でも型を構成したいときって、あるよね
Isabelle/HOLにsubset typeないかな〜と思って「Isabelle/HOL subset type」とか「Isabelle/HOL comprehension」とかで調べていましたが、全然見つからず、最終的にtypedefがその役割を担っていることが分かりました。これがあれば集合から型を作れるので、便利です。
Isabelle/HOLには他にもquotient typeがあるのですが、これはeffectiveでしょうか、そうではないのでしょうか。いずれ確認しましょう。今から楽しみですね。
この記事は個人サイトでも読めます。
この記事が気に入ったらサポートをしてみませんか?