Nuprl Definition : norm-list
norm-list(N) == λL.rec-case(L) of [] => [] | a::as => r.eval a' = N a in eval r' = r in [a' / r']
Definitions occuring in Statement :
list_ind: list_ind,
cons: [a / b],
nil: [],
callbyvalue: callbyvalue,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
list_ind: list_ind,
nil: [],
apply: f a,
callbyvalue: callbyvalue,
cons: [a / b]
FDL editor aliases :
norm-list
Latex:
norm-list(N) == \mlambda{}L.rec-case(L) of [] => [] | a::as => r.eval a' = N a in eval r' = r in [a' / r']
Date html generated:
2016_05_14-AM-07_41_09
Last ObjectModification:
2015_09_22-PM-05_53_55
Theory : list_1
Home
Index