---

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)
           (da i(k) = T))))

---

Definitions :  spreadn: spread3,  all: x:A. B[x],  l_member: (x  l),  fpf-domain: fpf-domain(f),  Knd: Knd,  assert: b,  isrcv: isrcv(k),  implies: P  Q,  Id: Id,  tagof: tag(k),  equal: s = t,  universe: Type,  fpf-ap: f(x),  apply: f a,  Kind-deq: KindDeq
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: 2010_08_27-AM-09_32_00
Last ObjectModification: 2009_12_16-AM-01_09_19

Home Index