Modular arithmetic: Difference between revisions

Content added Content deleted
Line 354: Line 354:


extern fn {tk : tkind}
extern fn {tk : tkind}
f : {m : int} modular_g0uint (tk, m) -<> modular_g0uint (tk, m)
f : {m : int} modular_g0uint (tk, m) -<> modular_g0uint (tk, m)


(* Using the "successor" function below means that, to add 1, we do
(* Using the "successor" function below means that, to add 1, we do