(* Generated by SimpleM backend *)
MODULE DEFINITION;

END DEFINITION.