Standard Library

ImandraX comes with a prelude of commonly used types and functions, available without any imports. This page provides an overview of the key modules.

List

The most commonly used module. Lists are the primary recursive data structure in IML.

Key functions

(* Construction *)
List.cons : 'a -> 'a list -> 'a list
(* Equivalent to :: *)
 
(* Basic operations *)
List.length : 'a list -> int
List.hd : 'a list -> 'a           (* head — first element *)
List.tl : 'a list -> 'a list      (* tail — all but first *)
List.rev : 'a list -> 'a list     (* reverse *)
List.append : 'a list -> 'a list -> 'a list  (* also @ *)
 
(* Higher-order *)
List.map : ('a -> 'b) -> 'a list -> 'b list
List.filter : ('a -> bool) -> 'a list -> 'a list
List.fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
List.fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
List.for_all : ('a -> bool) -> 'a list -> bool
List.exists : ('a -> bool) -> 'a list -> bool
 
(* Search *)
List.mem : 'a -> 'a list -> bool
List.find : ('a -> bool) -> 'a list -> 'a option
List.nth : 'a list -> int -> 'a
 
(* Transformation *)
List.flatten : 'a list list -> 'a list
List.sort : ('a -> 'a -> int) -> 'a list -> 'a list

Examples

eval List.length [1; 2; 3]        (* 3 *)
eval List.rev [1; 2; 3]           (* [3; 2; 1] *)
eval List.map (fun x -> x * 2) [1; 2; 3]  (* [2; 4; 6] *)
eval List.filter (fun x -> x > 2) [1; 2; 3; 4]  (* [3; 4] *)
eval List.fold_left (+) 0 [1; 2; 3]  (* 6 *)

Note on fold_right

In ImandraX, List.fold_right uses positional arguments (not named ~base as in Imandra Core). See Differences from Imandra Core.

Option

The option type for values that may or may not exist.

type 'a option = None | Some of 'a
 
Option.map : ('a -> 'b) -> 'a option -> 'b option
Option.bind : 'a option -> ('a -> 'b option) -> 'b option
Option.value : 'a option -> default:'a -> 'a
Option.is_some : 'a option -> bool
Option.is_none : 'a option -> bool

Int

Integer operations beyond basic arithmetic:

Int.abs : int -> int
Int.max : int -> int -> int
Int.min : int -> int -> int
Int.pow : int -> int -> int
Int.sqrt : int -> int     (* integer square root *)

Real

Real number operations (over the algebraic reals):

Real.abs : real -> real
Real.max : real -> real -> real
Real.min : real -> real -> real
Real.sqrt : real -> real
Real.pow : real -> int -> real

String

String.length : string -> int
String.append : string -> string -> string  (* also ^ *)
String.sub : string -> int -> int -> string
String.contains : string -> char -> bool

Map

Functional (immutable) maps:

Map.empty : ('k, 'v) Map.t
Map.add : 'k -> 'v -> ('k, 'v) Map.t -> ('k, 'v) Map.t
Map.find : 'k -> ('k, 'v) Map.t -> 'v option
Map.mem : 'k -> ('k, 'v) Map.t -> bool
Map.remove : 'k -> ('k, 'v) Map.t -> ('k, 'v) Map.t

Set

Functional (immutable) sets:

Set.empty : 'a Set.t
Set.add : 'a -> 'a Set.t -> 'a Set.t
Set.mem : 'a -> 'a Set.t -> bool
Set.remove : 'a -> 'a Set.t -> 'a Set.t
Set.union : 'a Set.t -> 'a Set.t -> 'a Set.t
Set.inter : 'a Set.t -> 'a Set.t -> 'a Set.t

Z.t and Q.t are types for integers and rationals respectively. In ImandraX, Q.t is not an alias for real — they are distinct types. ImandraX's real type is over the algebraic reals, not just the rationals. See Differences from Imandra Core.