Nuprl Definition : list-at

L1@L2 ==
  if null(L2) then []
  if null(L1) then []
  else if hd(L2)=0 then [hd(L1) / tl(L1)@tl(L2)] else tl(L1)@[hd(L2) - 1 / tl(L2)]
  fi

Definitions occuring in Statement : null: null(as), tl: tl(l), hd: hd(l), cons: [a / b], nil: [], ifthenelse: if b then t else f fi , int_eq: if a=b then c else d, subtract: n - m, natural_number: $n
Definitions occuring in definition : ifthenelse: if b then t else f fi , null: null(as), nil: [], int_eq: if a=b then c else d, cons: [a / b], subtract: n - m, hd: hd(l), natural_number: $n, tl: tl(l)
FDL editor aliases : list-at

Latex:
L1@L2 == if null(L2) then [] if null(L1) then [] else if hd(L2)=0 then [hd(L1) / tl(L1)@tl(L2)] else tl(L1)@[hd(L2) - 1 / tl(L2)] fi Date html generated: 2019_06_20-PM-01_20_50 Last ObjectModification: 2018_12_04-AM-11_31_58 Theory : list_1 Home Index