Nuprl Definition : mu-ge-print

mu-ge-print(f;n) ==
  fix((λmu-ge,n. if f n then n else eval m = n + 1 in eval s = evalall(nat-to-str(m)) in   print_line(s; mu-ge m) fi )) \000Cn


Definitions occuring in Statement :  nat-to-str: nat-to-str(n),  evalall: evalall(t),  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  add: n + m,  natural_number: $n,  callbyvalue: callbyvalue,  evalall: evalall(t),  nat-to-str: nat-to-str(n),  apply: f a
FDL editor aliases :  mu-ge-print
Latex:
mu-ge-print(f;n)  ==
    fix((\mlambda{}mu-ge,n.  if  f  n
                                then  n
                                else  eval  m  =  n  +  1  in
                                          eval  s  =  evalall(nat-to-str(m))  in
                                              print\_line(s;  mu-ge  m)
                                fi  )) 
    n


Date html generated: 2016_05_14-PM-03_36_02
Last ObjectModification: 2015_09_22-PM-06_01_19

Theory : decidable!equality


Home Index