私は抽出変換nat
を行っていますbig_int
ライブラリを使用したとき: ExtrOcamlNatBigInt、正しい型を返しませbig_int
んOcaml
nat_case
だから私はそれを修正します(ファイルExtrOcamlNatBigInt)が、Ocamlのライブラリには function がないため、関数を定義する方法が見つかりBig_int
ませんnat_case
。
Extract Inductive nat => "Big_int.big_int"
[ "Big_int.zero_big_int" "Big_int.succ_big_int" ] "Big_int.nat_case".
nat_case
byの 2 番目の定義を定義しようとしています。
Extract Inductive nat => "Big_int.big_int"
[ "Big_int.zero_big_int" "Big_int.succ_big_int" ] "(fun fO fS n ->
let one = Big_int.unit_big_int in
if n = Big_int.zero_big_int then fO () else fS (n - one))".
2 番目の定義を使用した後の結果を次に示します。
(** val nat_rect :
'a1 -> (Big_int.big_int -> 'a1 -> 'a1) -> Big_int.big_int -> 'a1 **)
let rec nat_rect f f0 n =
let one = Big_int.unit_big_int in
if n = Big_int.zero_big_int then f () else f0 (n - one)
(fun _ ->
f)
(fun n0 ->
f0 n0 (nat_rect f f0 n0)) n
n
次の行でエラーが発生しましたelse f0 (n - one)
:
ファイル "Datatypes.ml"、68 行目、51 ~ 52 文字目: エラー: この式には Big_int.big_int 型がありますが、int 型の式が予期されていました
minus
( -
) のせいだと思います。
minus
抽出も変更します:
Extract Constant minus => "fun n m -> Big_int.max_big_int Big_int.zero_big_int
(Big_int.sub_big_int n m)".
nat_case
の関数を定義するのを手伝ってくれませんBig_int
か? どうもありがとうございました。