Module Imandra_prelude

type 'a printer = Stdlib.Format.formatter -> 'a -> unit
module Caml : sig ... end
module Imandra_caml = Caml
module Caml_unix = Unix
module Caml_sys = Stdlib.Sys
module Unix : sig ... end
module Sys : sig ... end

Bare minimum needed for ordinals and validation

type nonrec int = Z.t

Builtin integer type, using arbitrary precision integers.

This type is an alias to Z.t (using Zarith).

NOTE: here Imandra diverges from normal OCaml, where integers width is bounded by native machine integers. "Normal" OCaml integers have type Caml.Int.t and can be entered using the 'i' suffix: 0i

val (=) : 'a -> 'a -> bool

Equality. Must be applied to non-function types.

val (<>) : 'a -> 'a -> bool
val not : bool -> bool
val implies : bool -> bool -> bool
val explies : bool -> bool -> bool
val iff : bool -> bool -> bool
val (+) : Z.t -> Z.t -> Z.t
val const : 'a -> 'b -> 'a

const x y returns x. In other words, const x is the constant function that always returns x.

val (>=) : int -> int -> bool
type nonrec nativeint = nativeint
val mk_nat : int -> int
type nonrec 'a option = 'a option =
| None
| Some of 'a
type 'a list = 'a Caml.list =
| []
| :: of 'a * 'a list
type nonrec float = float
type nonrec real = Q.t
type nonrec string = string
val (<) : int -> int -> bool
val (<=) : int -> int -> bool
val (>) : int -> int -> bool
val min : int -> int -> int
val max : int -> int -> int
val (<.) : real -> real -> bool
val (<=.) : real -> real -> bool
val (>.) : real -> real -> bool
val (>=.) : real -> real -> bool
val min_r : real -> real -> real
val max_r : real -> real -> real
val (~-) : Z.t -> Z.t
val abs : int -> int
val (-) : Z.t -> Z.t -> Z.t
val (~+) : Z.t -> Z.t
val (*) : Z.t -> Z.t -> Z.t
val (/) : Z.t -> Z.t -> Z.t

Euclidian division on integers, see http://smtlib.cs.uiowa.edu/theories-Ints.shtml

val (mod) : Z.t -> Z.t -> Z.t

Euclidian remainder on integers

val compare : int -> int -> Z.t

Total order

Ordinals

module Ordinal : sig ... end

We need to define ordinals before any recursive function is defined, because ordinals are used for termination proofs.

module Peano_nat : sig ... end

Other builtin types

type nonrec unit = unit =
| ()
type ('a, 'b) result = ( 'a, 'b ) Stdlib.result =
| Ok of 'a
| Error of 'b

Result type, representing either a successul result Ok x or an error Error x.

module Result : sig ... end
type ('a, 'b) either =
| Left of 'a
| Right of 'b

A familiar type for Haskellers

val (|>) : 'a -> ( 'a -> 'b ) -> 'b

Pipeline operator.

x |> f is the same as f x, but it composes nicely: x |> f |> g |> h can be more readable than h(g(f x)).

val (@@) : ( 'a -> 'b ) -> 'a -> 'b

Right-associative application operator.

f @@ x is the same as f x, but it binds to the right: f @@ g @@ h @@ x is the same as f (g (h x)) but with fewer parentheses.

val id : 'a -> 'a

Identity function. id x = x always holds.

val (%>) : ( 'a -> 'b ) -> ( 'b -> 'c ) -> 'a -> 'c

Mathematical composition operator.

f %> g is fun x -> g (f x)

val (==) : 'a -> 'b -> Caml.use_normal_equality
val (!=) : 'a -> 'b -> Caml.use_normal_equality
val (+.) : real -> real -> real
val (-.) : real -> real -> real
val (~-.) : Q.t -> Q.t
val (*.) : real -> real -> real
val (/.) : real -> real -> real
module List : sig ... end
val (@) : 'a list -> 'a list -> 'a list

Infix alias to List.append

val (--) : int -> int -> int list

Alias to List.(--)

module Int : sig ... end
module Bool : sig ... end
module Array : sig ... end
module Option : sig ... end
module Real : sig ... end
module Map : sig ... end
module Multiset : sig ... end

Sets

module Set : sig ... end
module String : sig ... end
val (^) : String.t -> String.t -> String.t

Alias to String.append

val succ : Z.t -> Z.t

Next integer

val pred : Z.t -> Z.t

Previous integer

val fst : ('a * 'b) -> 'a
val snd : ('a * 'b) -> 'b
module Float : sig ... end
module LChar : sig ... end

Logic-mode strings

Strings purely in Imandra.

module LString : sig ... end
module Pervasives : sig ... end
module Stdlib : sig ... end