Nuprl Definition : mon_htfor
HTFor{g} h::t ∈ as. f[h; t] == ForHdTl{A,*,e} h::t ∈ as. f[h; t]
Definitions occuring in Statement :
for_hdtl: ForHdTl{A,f,k} h::t ∈ as. g[h; t],
grp_id: e,
grp_op: *
Definitions occuring in definition :
for_hdtl: ForHdTl{A,f,k} h::t ∈ as. g[h; t],
grp_op: *,
grp_id: e
Latex:
HTFor\{g\} h::t \mmember{} as. f[h; t] == ForHdTl\{A,*,e\} h::t \mmember{} as. f[h; t]
Date html generated:
2016_05_16-AM-07_36_32
Last ObjectModification:
2015_09_23-AM-09_51_30
Theory : list_2
Home
Index