Function prop::path_semantics::ty_or_split_da

source · [−]
pub fn ty_or_split_da<A: DProp, B: Prop, C: Prop>(
    (ty_a_or_b_c, pord): Ty<A, Or<B, C>>
) -> Or<Ty<A, B>, Ty<A, C>>
Expand description

(a : (b ⋁ c)) => (a : b) ⋁ (a : c).