Idrisでゲーデルの不完全性定理を証明しました。Decは、引数が真ならYesと証明を、偽ならNoと反証を返します。 （実際に判定、証明してくれる訳ではありません） そして、Not . Decな命題とは、証明も反証もできない命題という事になります。Fixは不動点コン…