Function prop::imply::id

source · 
pub fn id<A: Prop>() -> Imply<A, A>
Expand description

a => a.

Examples found in repository?
examples/ps_bool.rs (line 69)
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76

    fn def_idb<X: LProp>(_idb: Self::Idb, f: Mem<X>) -> And<
        Imply<Q<X, Self::False>, Q<Inc<X>, Self::False>>,
        Imply<Q<X, Self::True>, Q<Inc<X>, Self::True>>,
    >
        where X: POrd<Inc<X>>
    {
        let f1 = f.0.clone();
        let f2 = f.0.clone();
        (Rc::new(move |eq_x_false| {
            let p = assume_naive();
            p((eq_x_false, (f1.clone(), imply::id())))
        }),
         Rc::new(move |eq_x_true| {
             let p = assume_naive();
             p((eq_x_true, (f2.clone(), imply::id())))
         })
        )
    }