coq2rust从Coq提取Rust程序

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<nat>) }

nat>