prop 0.47.0

Propositional logic with types in Rust
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
25
26
27
28
29
30
31

use prop::*;
use ava_modal::*;
use hooo::*;

// `¬¬¬◇a => ¬□a`.
pub fn proof1<A: DProp>(nnnpos_a: Not<Not<Not<Pos<A>>>>) -> Not<Nec<A>> {
    imply::in_left(nnnpos_a, |x: Nec<A>| {
        let x = npos_to_para(x);
        let x = para_rev_not(x);
        let x: Not<Not<Pos<A>>> = imply::in_left(x, npos_to_para);
        x
    })
}

// `¬◇a => ¬□a`.
pub fn proof2<A: DProp>(npos_a: Not<Pos<A>>) -> Not<Nec<A>> {
    proof1(not::double(npos_a))
}

/// `¬□a => ¬◇a`.
pub unsafe fn proof3<A: DProp>(nnec_a: Not<Nec<A>>) -> Not<Pos<A>> {
    let x = not::rev_triple(imply::in_left(nnec_a, |x: Not<Not<Pos<A>>>| {
        let x: Not<Para<A>> = imply::in_left(x, |y| para_to_npos(y));
        let x = pow_not(x);
        let x = para_to_npos(x);
        x
    }));
    x
}

fn main() {}