文件名称：coq-of-ocaml：将OCaml程序导入Coq
文件大小：1.2MB
文件格式：ZIP
更新时间：2024-02-21 07:29:44
compiler ocaml coq CompilerOCaml
食用辅酶 将OCaml程序导入Coq。 从文件main.ml开始： type 'a tree = | Leaf of 'a | Node of 'a tree * 'a tree let rec sum tree = match tree with | Leaf n -> n | Node ( tree1 , tree2 ) -> sum tree1 + sum tree2 跑： coq-of-ocaml main.ml 获取文件Main.v ： Require Import CoqOfOCaml.CoqOfOCaml. Require Import CoqOfOCaml.Settings. Inductive tree (a : Set ) : Set := | Leaf : a -> tree a | Node : tree a -> tree a -> tree a. Arguments Leaf {_}. Arguments Node {_}. Fixpoint sum (tree : tree int) : int := match tree