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 then inl (snd(p)) else fi ))) of
       [] => inr _.Ax) 
       a::L => r
        of inl(z) =>
        if lbl=a then inl <0, Ax, Ax> else inl let i,_,_ in <1, Ax, Ax> fi 
        inr(_) =>
        if lbl=a then inl <0, Ax, Ax> else inr _.Ax)  fi 
   of inl(x) =>
   inr(_) =>

Definitions occuring in Statement :  map: map(f;as) list_ind: list_ind outl: outl(x) ifthenelse: if then else fi  eq_atom: =a y spreadn: spread3 pi1: fst(t) pi2: snd(t) atom_eq: if a=b then else fi  lambda: λx.A[x] pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x add: m natural_number: $n axiom: Ax
Definitions occuring in definition :  map: map(f;as) outl: outl(x) list_ind: list_ind ifthenelse: if then else fi  eq_atom: =a y pi1: fst(t) pi2: snd(t) decide: case of inl(x) => s[x] inr(y) => t[y] spreadn: spread3 add: m atom_eq: if a=b then else fi  inl: inl x natural_number: $n pair: <a, b> inr: inr  lambda: λx.A[x] axiom: Ax
FDL editor aliases :  mrec-member

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  =>
                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)  =>
      |  inr($_{}$)  =>

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

Theory : tuples

Home Index