Nuprl Definition : p-compose'
f o' g == λx.if can-apply(g;x) then inl (f x do-apply(g;x)) else g x fi
Definitions occuring in Statement :
do-apply: do-apply(f;x),
can-apply: can-apply(f;x),
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: λx.A[x],
inl: inl x
Definitions occuring in definition :
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
can-apply: can-apply(f;x),
inl: inl x,
do-apply: do-apply(f;x),
apply: f a
FDL editor aliases :
p-compose'
Latex:
f o' g == \mlambda{}x.if can-apply(g;x) then inl (f x do-apply(g;x)) else g x fi
Date html generated:
2016_05_15-PM-03_29_05
Last ObjectModification:
2015_09_23-AM-07_43_43
Theory : general
Home
Index