DEFINITION MODULE TestIO;
(* Minimal test I/O for toto.mod: WriteString + WriteLn, bound to the
   runtime shim (same externals as stdlib/SysIO). *)

PROCEDURE WriteString (VAR s : ARRAY OF CHAR);
(* Writes s to standard output (no newline). *)

PROCEDURE WriteLn;
(* Writes a newline to standard output. *)

END TestIO.