Skip to main content

fun_ext_ty

prop::fun::fun_ext

Function fun_ext_ty 

Source 
pub fn fun_ext_ty<F: Prop, G: Prop, X: Prop, Y: Prop, A: Prop>() -> Ty<FunExt<F, G>, Pow<FunExtTy<F, G, X, Y, A>, Tauto<Eq<F, G>>>>
Expand description

fun_ext(f, g) : (f == g)^true -> fun_ext_ty(f, g).

Type of function extensionality.