Function prop::path_semantics::naive_comp

source · [−]

pub fn naive_comp<F1: Prop, F2: Prop, F3: Prop, F4: Prop, X1: Prop, X2: Prop>(
    f: PSemNaive<F1, F2, F3, F4>, 
    g: PSemNaive<F3, F4, X1, X2>, 
    f1_f3: Imply<F1, F3>, 
    f2_f4: Imply<F2, F4>, 
    f3_x1: Imply<F3, X1>, 
    f4_x2: Imply<F4, X2>
) -> PSemNaive<F1, F2, X1, X2>

Expand description

Composition using the naive core axiom.