Module pocket_prover::extract
source · [−]Expand description
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))
)
}))
}