Nuprl Definition : decl-set-read-allowed
decl-set-read-allowed(R;dd) ==
let S,ds,da = dd in
∀i:{i:Id| (i ∈ S)} . l_all(fpf-domain(da i); Knd; k.↑read-allowed(R;k;i;fpf-domain(ds i)))
Definitions occuring in Statement :
fpf-domain: fpf-domain(f),
Knd: Knd,
Id: Id,
l_member: (x ∈ l),
assert: ↑b,
spreadn: spread3,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a
FDL editor aliases :
decl-set-read-allowed
decl-set-read-allowed(R;dd) ==
let S,ds,da = dd in
\mforall{}i:\{i:Id| (i \mmember{} S)\} . l\_all(fpf-domain(da i); Knd; k.\muparrow{}read-allowed(R;k;i;fpf-domain(ds i)))
Date html generated:
2015_07_17-AM-11_57_32
Last ObjectModification:
2013_03_27-AM-10_39_11
Home
Index