Nuprl Definition : ml-gcd
ml-gcd(a;b) == fix((λgcd,a,b. if (b =z 0) then a else gcd(b)(a rem b) fi ))(a)(b)
Definitions occuring in Statement :
ml_apply: f(x),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
fix: fix(F),
lambda: λx.A[x],
remainder: n rem m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
natural_number: $n,
ml_apply: f(x),
remainder: n rem m
FDL editor aliases :
ml-gcd
Latex:
ml-gcd(a;b) == fix((\mlambda{}gcd,a,b. if (b =\msubz{} 0) then a else gcd(b)(a rem b) fi ))(a)(b)
Date html generated:
2017_09_29-PM-05_51_28
Last ObjectModification:
2017_05_21-PM-04_12_39
Theory : ML
Home
Index