Nuprl Definition : nat-pred
n-1 == if n=0 then 0 else (n - 1)
Definitions occuring in Statement :
int_eq: if a=b then c else d,
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
subtract: n - m,
int_eq: if a=b then c else d
FDL editor aliases :
nat-pred
Latex:
n-1 == if n=0 then 0 else (n - 1)
Date html generated:
2017_04_21-AM-11_21_07
Last ObjectModification:
2017_04_20-PM-03_34_52
Theory : continuity
Home
Index