Nuprl Definition : normal-decl-set
normal-decl-set(dd) == let S,ds,da = dd in ∀i:{i:Id| (i ∈ S)} . (Normal(ds i) ∧ Normal(da i))
Definitions occuring in Statement :
normal-da: Normal(da),
normal-ds: Normal(ds),
Id: Id,
l_member: (x ∈ l),
spreadn: spread3,
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a
FDL editor aliases :
normal-decl-set
normal-decl-set(dd) == let S,ds,da = dd in \mforall{}i:\{i:Id| (i \mmember{} S)\} . (Normal(ds i) \mwedge{} Normal(da i))
Date html generated:
2015_07_17-AM-11_57_21
Last ObjectModification:
2013_03_27-AM-10_39_07
Home
Index