Function prop::fun::app2_fun_ty

source ·
pub fn app2_fun_ty<F: Prop, X: Prop, Y: Prop, Z: Prop, A: Prop, B: Prop>(
    ty_f: Ty<F, Pow<Pow<Z, Y>, X>>,
    ty_a: Ty<A, X>,
    ty_b: Ty<B, Y>
) -> Ty<App2<F, A, B>, Z>
Expand description

(f : x -> y -> z) ⋀ (a : x) ⋀ (b : y) => f(a)(b) : z.

Get type of applied binary operator.