Skip to main content

and

prop::path_semantics::ty

Function and 

Source 
pub fn and<X: Prop, Y: Prop, A: Prop, B: Prop>(
    (xa, pord_xa): Ty<X, A>,
    (yb, pord_yb): Ty<Y, B>,
) -> Ty<And<X, Y>, And<A, B>>
Expand description

(x : a) ⋀ (y : b) => ((x ⋀ y) : (a ⋀ b)).