Nuprl Definition : ffor
ffor(b0;b1;up;zs) == Y (λffor,zs. case zs of [] => b0 | z::zs' => up [z] zs' (b1 z) (ffor zs') esac) zs
Definitions occuring in Statement :
list_ind: list_ind,
cons: [a / b],
nil: [],
ycomb: Y,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
ycomb: Y,
lambda: λx.A[x],
list_ind: list_ind,
cons: [a / b],
nil: [],
apply: f a
Latex:
ffor(b0;b1;up;zs) == Y (\mlambda{}ffor,zs. case zs of [] => b0 | z::zs' => up [z] zs' (b1 z) (ffor zs') esac\000C) zs
Date html generated:
2016_05_16-AM-07_51_32
Last ObjectModification:
2015_09_23-AM-09_52_20
Theory : mset
Home
Index