先日Coqの関数をOCamlのコードとして出力してみました。サンプルとしては (* ret_num.v *) Definition ret_num (n : nat) : nat := n. Extraction "ret_num.ml" ret_num. を coqc ret_num.vして (* ret_num.ml *) type nat = | O | S of nat (** val ret_num…