18/06/29 07:10:56.55 iQFgCDGa.net
>>330
質問の答えになっているか分からないですが、
今回の方法だと、再帰関数を書き終えた時点で証明モードに入って、そこでの証明を終えると、関数が定義されます。
具体的には、Coq.Program.Wfをインポートして、減少する引数をmeasureで指定して、Program Fixpointで関数を書きます。
URLﾘﾝｸ(www.google.com)URLﾘﾝｸ(d.hatena.ne.jp)
18/06/29 07:10:56.55 iQFgCDGa.net
>>330
質問の答えになっているか分からないですが、
今回の方法だと、再帰関数を書き終えた時点で証明モードに入って、そこでの証明を終えると、関数が定義されます。
具体的には、Coq.Program.Wfをインポートして、減少する引数をmeasureで指定して、Program Fixpointで関数を書きます。
URLﾘﾝｸ(www.google.com)URLﾘﾝｸ(d.hatena.ne.jp)