Nuprl Definition : co-w-select
w@s == fix((λco-w-select,w,s. if null(s) ∨bisl(w) then w else co-w-select (outr(w) hd(s)) tl(s) fi )) w s
Definitions occuring in Statement :
hd: hd(l),
null: null(as),
tl: tl(l),
bor: p ∨bq,
outr: outr(x),
ifthenelse: if b then t else f fi ,
isl: isl(x),
apply: f a,
fix: fix(F),
lambda: λx.A[x]
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
bor: p ∨bq,
null: null(as),
isl: isl(x),
apply: f a,
outr: outr(x),
hd: hd(l),
tl: tl(l)
FDL editor aliases :
co-w-select
Latex:
w@s == fix((\mlambda{}co-w-select,w,s. if null(s) \mvee{}\msubb{}isl(w) then w else co-w-select (outr(w) hd(s)) tl(s) fi \000C)) w s
Date html generated:
2016_05_15-PM-10_05_41
Last ObjectModification:
2015_09_23-AM-08_22_11
Theory : bar!induction
Home
Index