Nuprl Definition : first-eclass

first-eclass(Xs) ==
  λeo,e. accumulate (with value b and list item X):
          if (#(b) =_z 1) then b else X eo e fi
         over list:
           Xs
         with starting value:
          {})

Definitions occuring in Statement : list_accum: list_accum, ifthenelse: if b then t else f fi , eq_int: (i =_z j), apply: f a, lambda: λx.A[x], natural_number: $n, bag-size: #(bs), empty-bag: {}
FDL editor aliases : first-eclass

Latex:
first-eclass(Xs) == \mlambda{}eo,e. accumulate (with value b and list item X): if (\#(b) =\msubz{} 1) then b else X eo e fi over list: Xs with starting value: \{\}) Date html generated: 2015_07_20-PM-03_17_28 Last ObjectModification: 2012_02_25-PM-01_40_07 Home Index