0142132人目の素数さん垢版 | 大砲2015/06/19(金) 00:07:06.67ID:KgdfsOzM >>140 このライブラリを使えばいいんじゃないかな、 https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.ConstructiveEpsilon.html nステップ以下で停止するって述語が Hypothesis P_dec : forall n, {P n}+{~(P n)}. を満たしていれば、停止するステップ数を構成してくれるよ。