pocket_prover-set

为PocketProver推理集合属性的基础逻辑系统

extern crate pocket_prover;
extern crate pocket_prover_set;

use pocket_prover::*;
use pocket_prover_set::*;

fn main() {
    println!("Result {}", Set::imply(
        |s| s.fin_many,
        |s| not(s.inf_many)
    ));
}

有4个信息位，用于推导所有其他属性

• any - 所有类型，包括未定义的类型
• uniq - 唯一值
• fin_many - 有限多个值
• inf_many - 无限多个值

当所有位都设置为0时，集合为空（.none()）。

当至少有一个位设置为1时，集合为非空（.some()）。

当它为any但既不是唯一、有限也不是无限时，集合为未定义。

以下是一个8个集合的证明示例

extern crate pocket_prover;
extern crate pocket_prover_set;

use pocket_prover::*;
use pocket_prover_set::*;

fn main() {
    println!("Result {}", <(Set, Set, Set, Set, Set, Set, Set, Set)>::imply(
        |sets| and(sets.uniqs(|xs| xorn(xs)), sets.0.uniq),
        |sets| not(sets.7.uniq)
    ));
}