---

maybe-new(s;avoid) ==
  if deq-member(NameDeq;s;avoid)
  then let n = mu(n.(deq-member(NameDeq;s @ nat-to-str(n);avoid))) in
           s @ nat-to-str(n)
  else s
  fi 

---

Definitions :  ifthenelse: if b then t else f fi ,  let: let,  mu: mu(f),  lambda: x.A[x],  bnot: b,  deq-member: deq-member(eq;x;L),  name-deq: NameDeq,  append: as @ bs,  nat-to-str: nat-to-str(n)
FDL editor aliases :  maybe-new

---

maybe-new(s;avoid)  ==
    if  deq-member(NameDeq;s;avoid)
    then  let  n  =  mu(\mlambda{}n.(\mneg{}\msubb{}deq-member(NameDeq;s  @  nat-to-str(n);avoid)))  in
                      s  @  nat-to-str(n)
    else  s
    fi 


Date html generated: 2010_08_26-PM-11_31_13
Last ObjectModification: 2010_02_16-PM-01_28_26

Home Index