Nuprl Definition : doublefact
doublefact(n) ==  if n <z 2 then 1 else n * doublefact(n - 2) fi 
Definitions occuring in Statement : 
ifthenelse: if b then t else f fi 
, 
lt_int: i <z j
, 
multiply: n * m
, 
subtract: n - m
, 
natural_number: $n
Definitions occuring in definition : 
ifthenelse: if b then t else f fi 
, 
lt_int: i <z j
, 
multiply: n * m
, 
subtract: n - m
, 
natural_number: $n
FDL editor aliases : 
doublefact
Latex:
doublefact(n)  ==    if  n  <z  2  then  1  else  n  *  doublefact(n  -  2)  fi 
Date html generated:
2019_06_20-PM-02_30_48
Last ObjectModification:
2019_01_04-PM-06_42_00
Theory : num_thy_1
Home
Index