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