Nuprl Definition : lnk-decl
lnk-decl(l;dt) == <map(λtg.rcv(l,tg);fst(dt)), λk.dt(snd(outl(k)))>
Definitions occuring in Statement :
fpf-ap: f(x),
rcv: rcv(l,tg),
id-deq: IdDeq,
map: map(f;as),
outl: outl(x),
pi1: fst(t),
pi2: snd(t),
lambda: λx.A[x],
pair: <a, b>
FDL editor aliases :
lnk-decl
lnk-decl(l;dt) == <map(\mlambda{}tg.rcv(l,tg);fst(dt)), \mlambda{}k.dt(snd(outl(k)))>
Date html generated:
2015_07_17-AM-11_15_12
Last ObjectModification:
2012_02_25-AM-11_13_50
Home
Index