Nuprl Definition : es-decl-set-declares-tag
es-decl-set-declares-tag{i:l}(dd;b;T) ==
let S,ds,da = dd in
∀i:Id. ((i ∈ S) ⇒ (∀k:Knd. ((k ∈ fpf-domain(da i)) ⇒ (↑isrcv(k)) ⇒ (tag(k) = b ∈ Id) ⇒ (da i(k) = T ∈ Type))))
Definitions occuring in Statement :
fpf-ap: f(x),
fpf-domain: fpf-domain(f),
Kind-deq: KindDeq,
tagof: tag(k),
isrcv: isrcv(k),
Knd: Knd,
Id: Id,
l_member: (x ∈ l),
assert: ↑b,
spreadn: spread3,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
universe: Type,
equal: s = t ∈ T
FDL editor aliases :
es-decl-set-declares-tag
es-decl-set-declares-tag\{i:l\}(dd;b;T) ==
let S,ds,da = dd in
\mforall{}i:Id
((i \mmember{} S) {}\mRightarrow{} (\mforall{}k:Knd. ((k \mmember{} fpf-domain(da i)) {}\mRightarrow{} (\muparrow{}isrcv(k)) {}\mRightarrow{} (tag(k) = b) {}\mRightarrow{} (da i(k) = T))))
Date html generated:
2015_07_17-AM-11_56_30
Last ObjectModification:
2013_03_27-AM-10_38_44
Home
Index