Why3 Standard Library index
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.8.0