Function prop::quality::right

source · 
pub fn right<A: Prop, B: Prop>(q_ab: Q<A, B>) -> Q<B, B>
Expand description

(a ~~ b) => (b ~~ b).

Examples found in repository?
examples/ps_uniq_q.rs (line 41)
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54

pub fn proof<A: Prop, B: Prop, C: Prop>(
    f: impl UniqQ<B, A>,
    g: impl UniqQ<B, C>,
    sesh_ac: Not<Q<A, C>>
) -> And<Not<Q<B, A>>, Not<Q<B, C>>> {
    let sesh_ac2 = sesh_ac.clone();
    (
        Rc::new(move |q_ba| {
            let q_ab = symmetry(q_ba);
            let sesh_bc = nq_left(q_ab.clone(), sesh_ac.clone());
            let q_bb = right(q_ab);
            let q_bc = g.uniq_q(q_bb);
            sesh_bc(q_bc)
        }),
        Rc::new(move |q_bc| {
            let q_cb = symmetry(q_bc);
            let sesh_ca = nq_symmetry(sesh_ac2.clone());
            let sesh_ba = nq_left(q_cb.clone(), sesh_ca.clone());
            let q_bb = right(q_cb);
            let q_ba = f.uniq_q(q_bb);
            sesh_ba(q_ba)
        }),
    )
}