poi 0.25.0

A pragmatic point-free theorem prover assistant
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12

use poi::prelude::*;

fn main() {
    let ref std = std();

    // and(true, true) = true
    let a = app(And, (true, true)).reduce_all(std);

    // and(true)(true) = true
    let a = a.inline(&And, std).unwrap().reduce_all(std);
    assert_eq!(a, true.into());
}