Why3 Standard Library index


Basic I/O Functions

module StdIO

  use string.String
  use string.Char
  use int.Int

  type t = private {ghost mutable foo:int}
  val ghost bar:t

small trick so that printing vals are extracted to OCaml

  val print_string (s: string) : unit
    writes { bar }

prints a string to the standard output

  val print_char (c: char) : unit
    writes { bar }

prints a char to the standard output

  val print_newline (_u:unit) : unit
    writes { bar }

prints a newline character to the standard output, and flushes it

  val print_int (i: int) : unit
    writes { bar }

prints a Why3 int to the standard output

end

Generated by why3doc 1.7.1