pocket_prover 0.18.0

A fast, brute force, automatic theorem prover for first order logic
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

/*

A set type is a type where
when two members are equal, they have the same properties.

Set types are homotopy level 2.

*/

use pocket_prover::*;

fn main() {
    println!("{}", measure(1, || prove!(&mut |a, b, x| {
        imply(
            and!(
                is_set(x, a, b),
                imply(a, x),
                imply(b, x),
                eq(a, b)
            ),
            hom_eq(2, a, b)
        )
    })))
}