Nuprl Definition : mrec-member

mrec-member(s;n;lbl) ==
  case rec-case(map(λp.(fst(p));outl(rec-case(s) of
                                     [] => inr Ax 
                                     p::ps =>
                                      r.if fst(p) =a n then inl (snd(p)) else r fi ))) of
       [] => inr (λ_.Ax) 
       a::L =>
        r.case r
        of inl(z) =>
        if lbl=a then inl <0, Ax, Ax> else inl let i,_,_ = z in <i + 1, Ax, Ax> fi 
        | inr(_) =>
        if lbl=a then inl <0, Ax, Ax> else inr (λ_.Ax)  fi 
   of inl(x) =>
   x
   | inr(_) =>
   Ax


Definitions occuring in Statement :  map: map(f;as),  list_ind: list_ind,  outl: outl(x),  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  spreadn: spread3,  pi1: fst(t),  pi2: snd(t),  atom_eq: if a=b then c else d fi ,  lambda: λx.A[x],  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  add: n + m,  natural_number: $n,  axiom: Ax
Definitions occuring in definition :  map: map(f;as),  outl: outl(x),  list_ind: list_ind,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  pi1: fst(t),  pi2: snd(t),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spreadn: spread3,  add: n + m,  atom_eq: if a=b then c else d fi ,  inl: inl x,  natural_number: $n,  pair: <a, b>,  inr: inr x ,  lambda: λx.A[x],  axiom: Ax
FDL editor aliases :  mrec-member
Latex:
mrec-member(s;n;lbl)  ==
    case  rec-case(map(\mlambda{}p.(fst(p));outl(rec-case(s)  of
                                                                          []  =>  inr  Ax 
                                                                          p::ps  =>
                                                                            r.if  fst(p)  =a  n  then  inl  (snd(p))  else  r  fi  )))  of
              []  =>  inr  (\mlambda{}$_{}$.Ax) 
              a::L  =>
                r.case  r
                of  inl(z)  =>
                if  lbl=a  then  inl  ɘ,  Ax,  Ax>  else  inl  let  i,$_{}$,$_{}\mbackslash{}\000Cff24  =  z  in  <i  +  1,  Ax,  Ax>  fi 
                |  inr($_{}$)  =>
                if  lbl=a  then  inl  ɘ,  Ax,  Ax>  else  inr  (\mlambda{}$_{}$.Ax)    fi 
      of  inl(x)  =>
      x
      |  inr($_{}$)  =>
      Ax


Date html generated: 2019_06_20-PM-02_15_04
Last ObjectModification: 2019_02_27-PM-02_21_25

Theory : tuples


Home Index