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.