Nuprl Definition : maybe_new_var
maybe_new_var(v;vs) ==
  if null(vs)
  then v
  else eval t = if v is an atom then v otherwise fst(v) in
       let n,x = list-max(b.var-num(t;b);vs) 
       in if n <z 0 then v else <t, n> fi 
  fi 
Definitions occuring in Statement : 
var-num: var-num(t;b)
, 
list-max: list-max(x.f[x];L)
, 
null: null(as)
, 
callbyvalue: callbyvalue, 
ifthenelse: if b then t else f fi 
, 
lt_int: i <z j
, 
pi1: fst(t)
, 
isatom: if z is an atom then a otherwise b
, 
spread: spread def, 
pair: <a, b>
, 
natural_number: $n
Definitions occuring in definition : 
null: null(as)
, 
callbyvalue: callbyvalue, 
isatom: if z is an atom then a otherwise b
, 
pi1: fst(t)
, 
spread: spread def, 
list-max: list-max(x.f[x];L)
, 
var-num: var-num(t;b)
, 
ifthenelse: if b then t else f fi 
, 
lt_int: i <z j
, 
natural_number: $n
, 
pair: <a, b>
FDL editor aliases : 
maybe_new_var
Latex:
maybe\_new\_var(v;vs)  ==
    if  null(vs)
    then  v
    else  eval  t  =  if  v  is  an  atom  then  v  otherwise  fst(v)  in
              let  n,x  =  list-max(b.var-num(t;b);vs) 
              in  if  n  <z  0  then  v  else  <t,  n>  fi 
    fi 
Date html generated:
2020_05_19-PM-09_53_14
Last ObjectModification:
2020_03_09-PM-04_08_02
Theory : terms
Home
Index