---

esharp-comb-wf(env;F;ra) ==
  case apply-alist(AtomDeq;env;F)
  of inl(found) => case found
                   of inl(bd) => False
                    | inr(z) => case z
                                of inl(combdef) => let n,m,rec,wf,T,f = ... in 
                                                   (||ra|| = (n + m))
                                                    (wf 
                                                      map(dv.hd(cdv-types(dv));
                                                          ra))
                                 | inr(dv) => False
   | inr(z) => False

---

Definitions :  apply-alist: apply-alist(eq;L;x),  atom-deq: AtomDeq,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spreadn: spread6,  and: P  Q,  equal: s = t,  int: ,  length: ||as||,  add: n + m,  apply: f a,  map: map(f;as),  lambda: x.A[x],  hd: hd(l),  cdv-types: cdv-types(dv),  false: False
FDL editor aliases :  esharp-comb-wf

---

esharp-comb-wf(env;F;ra)  ==
    case  apply-alist(AtomDeq;env;F)
    of  inl(found)  =>  case  found
                                      of  inl(bd)  =>  False
                                        |  inr(z)  =>  case  z
                                                                of  inl(combdef)  =>  let  n,m,rec,wf,T,f  =  combdef  in 
                                                                                                      (||ra||  =  (n  +  m))
                                                                                                      \mwedge{}  (wf  map(\mlambda{}dv.hd(cdv-types(dv));ra))
                                                                  |  inr(dv)  =>  False
      |  inr(z)  =>  False


Date html generated: 2010_08_27-PM-08_16_34
Last ObjectModification: 2010_06_22-PM-02_23_37

Home Index