Module Imandrax_ocaml_prelude.Prelude_extracted

module Program_prelude_ : sig ... end

Bare minimum needed for ordinals and validation

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

type nonrec bool = bool

Builtin boolean type.

type nonrec unit = unit =
  1. | ()
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 (+) : int -> int -> int
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
val mk_nat : int -> int
type nonrec 'a option = 'a option =
  1. | None
  2. | Some of 'a
type 'a list = 'a Program_prelude_.List.t =
  1. | []
  2. | :: 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 (~-) : int -> int
val abs : int -> int
val (-) : int -> int -> int
val (~+) : int -> int
val (*) : int -> int -> int
val (/) : int -> int -> int

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

val (mod) : int -> int -> int

Euclidian remainder on integers

val compare : int -> int -> int

Total order

type ('a, 'b) result = ('a, 'b) Stdlib.result =
  1. | Ok of 'a
  2. | Error of 'b

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

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

module Result : sig ... end
type ('a, 'b) either =
  1. | Left of 'a
  2. | 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 -> 'a -> bool
val (!=) : 'a -> 'a -> bool
val (+.) : real -> real -> real
val (-.) : real -> real -> real
val (~-.) : real -> real
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 : int -> int

Next integer

val pred : int -> int

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