ps_comp/
ps_comp.rs

1use prop::*;
2use path_semantics::*;
3
4/// Compose 3 layers of propositions into 2 layers.
5pub fn proof<A: LProp, B: LProp, C: LProp, F2: LProp, X2: LProp, Y2: LProp>(
6    a_b: Imply<A, B>,
7    f2_x2: Imply<F2, X2>,
8    b_c: Imply<B, C>,
9    x2_y2: Imply<X2, Y2>
10) -> PSemNaive<A, F2, C, Y2>
11    where A::N: nat::Lt<B::N>,
12          B::N: nat::Lt<C::N>,
13          F2::N: nat::Lt<X2::N>,
14          X2::N: nat::Lt<Y2::N>,
15{
16    naive_comp(assume_naive(), assume_naive(),
17               a_b, f2_x2, b_c, x2_y2)
18}
19
20fn main() {}