Nuprl Definition : es-interface-unmatched

es-interface-unmatched(A; B; R) ==
  es-interface-accum(λL,v. let L' = if oob-hasleft(v) then L @ [oob-getleft(v)] else L fi  in
                               if oob-hasright(v) then remove-first(λa.(R a oob-getright(v));L') else L' fi ;[];(A | B))


Definitions occuring in Statement :  es-interface-accum: es-interface-accum(f;x;X),  es-interface-or: (X | Y),  remove-first: remove-first(P;L),  append: as @ bs,  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  let: let,  apply: f a,  lambda: λx.A[x],  oob-getright: oob-getright(x),  oob-hasright: oob-hasright(x),  oob-getleft: oob-getleft(x),  oob-hasleft: oob-hasleft(x)
Latex:
es-interface-unmatched(A;  B;  R)  ==
    es-interface-accum(\mlambda{}L,v.  let  L'  =  if  oob-hasleft(v)  then  L  @  [oob-getleft(v)]  else  L  fi    in
                                                              if  oob-hasright(v)
                                                              then  remove-first(\mlambda{}a.(R  a  oob-getright(v));L')
                                                              else  L'
                                                              fi  ;[];(A  |  B))


Date html generated: 2015_07_20-PM-03_51_30
Last ObjectModification: 2012_02_25-PM-01_56_51

Home Index