---

esharp-comb(env;
F;ra) ==
  case apply-alist(AtomDeq;env;F)
  of inl(found) =>
   case found
   of inl(bd) =>
    []
    | inr(z) =>
    case z
    of inl(combdef) =>
     let n,m,rec,wf,T,f = combdef in 
     let ts = map(dv.hd(cdv-types(dv));ra) in
      let T' = T ts in
      let argtype = k:||ts||  bag(ts[k]) in
      let arg = pack-cdv-args(n;m;ra) in
      ...
     | inr(dv) =>
     []
   | inr(z) =>
   []

---

Definitions occuring in Statement :  pack-cdv-args: pack-cdv-args(n;m;L),  cdv-types: cdv-types(dv),  cdvreccomb: cdvreccomb(typ;argtype;arg;fun),  cdvcomb: cdvcomb(typ;argtype;arg;fun),  select: l[i],  hd: hd(l),  map: map(f;as),  length: ||as||,  ifthenelse: if b then t else f fi ,  int_seg: {i..j},  let: let,  spreadn: spread6,  apply: f a,  lambda: x.A[x],  function: x:A  B[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  nil: [],  natural_number: $n,  apply-alist: apply-alist(eq;L;x),  atom-deq: AtomDeq,  bag: bag(T)
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,  map: map(f;as),  lambda: x.A[x],  hd: hd(l),  cdv-types: cdv-types(dv),  apply: f a,  function: x:A  B[x],  int_seg: {i..j},  natural_number: $n,  length: ||as||,  bag: bag(T),  select: l[i],  let: let,  pack-cdv-args: pack-cdv-args(n;m;L),  ifthenelse: if b then t else f fi ,  cdvreccomb: cdvreccomb(typ;argtype;arg;fun),  cdvcomb: cdvcomb(typ;argtype;arg;fun),  nil: []
FDL editor aliases :  esharp-comb

---

esharp-comb(env;
F;ra)  ==
    case  apply-alist(AtomDeq;env;F)
    of  inl(found)  =>
      case  found
      of  inl(bd)  =>
        []
        |  inr(z)  =>
        case  z
        of  inl(combdef)  =>
          let  n,m,rec,wf,T,f  =  combdef  in 
          let  ts  =  map(\mlambda{}dv.hd(cdv-types(dv));ra)  in
            let  T'  =  T  ts  in
            let  argtype  =  k:\mBbbN{}||ts||  {}\mrightarrow{}  bag(ts[k])  in
            let  arg  =  pack-cdv-args(n;m;ra)  in
            if  rec  then  cdvreccomb(T';argtype;arg;f)  else  cdvcomb(T';argtype;arg;f)  fi 
          |  inr(dv)  =>
          []
      |  inr(z)  =>
      []


Date html generated: 2011_08_17-PM-04_32_46
Last ObjectModification: 2011_01_19-PM-09_14_09

Home Index