Nuprl Definition : cdv-classes-and-programs

cdv-classes-and-programs(dv) ==
  case(dv)
  Base(a)=> [<base-deriv-type(a), base-deriv-class(a), base-deriv-program(a)>]
  pair(d1,d2) => cs1,cs2.cs1 @ cs2
  (d)'=> cs.map(

c.let T,X,prg = c in
                   <T, (X)', delay-program(prg)>;cs)
  f(d:P):T=> cps.[<T
                  , simple-comb(f;

k.(fst(snd(cps[k]))))
, simple-comb-program(f;T;map(

cp.(snd(snd(cp)));cps))>]
f(d:P, self'):T=> cps.[<T
, f(

k.(fst(snd(cps[k])));(self)')
, rec-comb-program(f;T;map(

cp.(snd(snd(cp)));cps))>]

Definitions : classderiv_ind: classderiv_ind, base-deriv-type: base-deriv-type(bdv), base-deriv-class: base-deriv-class(bdv), base-deriv-program: base-deriv-program(bdv), append: as @ bs, spreadn: spread3, es-prior-val: (X)', delay-program: delay-program(P), simple-comb: simple-comb(F; Xs), simple-comb-program: simple-comb-program(F;B;Ps), cons: [car / cdr], pair: <a, b>, rec-combined-class: f(X;(self)'), pi1: fst(t), select: l[i], rec-comb-program: rec-comb-program(F;B;Ps), map: map(f;as), lambda:

x.A[x], pi2: snd(t), nil: []
FDL editor aliases : cdv-classes-and-programs

cdv-classes-and-programs(dv) == case(dv) Base(a)=> [<base-deriv-type(a), base-deriv-class(a), base-deriv-program(a)>] pair(d1,d2) => cs1,cs2.cs1 @ cs2 (d)'=> cs.map(\mlambda{}c.let T,X,prg = c in <T, (X)', delay-program(prg)>cs) f(d:P):T=> cps.[<T , simple-comb(f; \mlambda{}k.(fst(snd(cps[k])))) , simple-comb-program(f;T;map(\mlambda{}cp.(snd(snd(cp)));cps))>] f(d:P, self'):T=> cps.[<T , f(\mlambda{}k.(fst(snd(cps[k])));(self)') , rec-comb-program(f;T;map(\mlambda{}cp.(snd(snd(cp)));cps))>] Date html generated: 2010_08_27-PM-08_14_29 Last ObjectModification: 2010_06_23-PM-03_47_01 Home Index