Module pocket_prover::extract

Helper utilities for extracting data from proofs.

use pocket_prover::*;

fn main() {
    println!("(a ∧ c) (b ∧ c) (∃)");
    println_extract!(
        &mut |a, b, c| and(eq(a, b), c);
        x0 => and(a, c),
        x1 => and(b, c)
    );

    println!("");
    println!("By looking at the table above one can see that `a ∧ c` and `b ∧ c` are equal.");
    println!("Therefore, one can prove:");
    println!("");
    println!("   (a = b) ∧ c");
    println!("-----------------");
    println!("(a ∧ c) = (b ∧ c)");
    println!("");
    println!("Result: {}", prove!(&mut |a, b, c| {
        imply(
            and(eq(a, b), c),
            eq(and(a, c), and(b, c))
        )
    }))
}

Functions

bit	Converts a boolean to a bit.
bitf	If the bit argument is 0, returns not, else id.
bitv	Converts a bit to a boolean.