coq of ocaml:将OCaml程序导入Coq 源码

食用辅酶 将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 CoqOfO