Nuprl Definition : var-num

var-num(t;b) ==
  if b is an atom then if b =a t then 0 else -1 fi  otherwise let x,n = b 
                                                              in if x =a t then n + 1 else -1 fi 


Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  isatom: if z is an atom then a otherwise b,  spread: spread def,  add: n + m,  minus: -n,  natural_number: $n
Definitions occuring in definition :  isatom: if z is an atom then a otherwise b,  spread: spread def,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  add: n + m,  minus: -n,  natural_number: $n
FDL editor aliases :  var-num
Latex:
var-num(t;b)  ==
    if  b  is  an  atom  then  if  b  =a  t  then  0  else  -1  fi    otherwise  let  x,n  =  b 
                                                                                                                            in  if  x  =a  t  then  n  +  1  else  -1  fi 


Date html generated: 2020_05_19-PM-09_53_12
Last ObjectModification: 2020_03_09-PM-04_08_02

Theory : terms


Home Index