Nuprl Definition : public-decls
public-decls(R;dd) ==
let S,ds,da = dd in
∀i:{i:Id| (i ∈ S)}
(l_all(fpf-domain(da i); Knd; k.(¬↑write-restricted(R;i;k)) ∧ (¬↑send-restricted(R;i;k)))
∧ l_all(fpf-domain(ds i); Id; y.¬↑read-restricted(R;i;y)))
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],
not: ¬A,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a
FDL editor aliases :
public-decls
public-decls(R;dd) ==
let S,ds,da = dd in
\mforall{}i:\{i:Id| (i \mmember{} S)\}
(l\_all(fpf-domain(da i); Knd; k.(\mneg{}\muparrow{}write-restricted(R;i;k)) \mwedge{} (\mneg{}\muparrow{}send-restricted(R;i;k)))
\mwedge{} l\_all(fpf-domain(ds i); Id; y.\mneg{}\muparrow{}read-restricted(R;i;y)))
Date html generated:
2015_07_17-AM-11_58_15
Last ObjectModification:
2013_03_27-AM-10_39_23
Home
Index