文件名称：coq2rust:Coq 到 Rust 程序提取。 整个树都在原始 Coq 代码库上
文件大小：6.08MB
文件格式：ZIP
更新时间：2024-07-24 17:39:00
OCaml
coq2rust
有关提取的 Coq 术语的示例，请参见input.v 。
尝试
$ ./configure -local
$ ./compile.sh
在包含此文件的目录中。 在此之后，test.rs 将包含如下提取的代码：
enum Empty_set<> {
}
enum Unit<> {
Tt
}
enum Bool<> {
True,
False
}
fn xorb(b1: Bool, b2: Bool) -> Bool {
match b1 {
Bool::True =>
(match b2 {
Bool::True => Bool::False,
Bool::False => Bool::True
}),
Bool::False => b2
}
}
enum Nat<> {
O,
S(Box