Basics

This page covers the fundamental building blocks of IML: values, basic types, expressions, arithmetic, and conditionals.

Values and bindings

Use let to bind a value to a name:

let x = 42
let greeting = "hello"
let flag = true

Bindings are immutable — once defined, a value cannot change. This is fundamental to IML's role as a logic.

Basic types

IML has several built-in types:

Type	Description	Examples
`int`	Arbitrary-precision integers	`0`, `42`, `-7`
`real`	Algebraic reals (rational constants)	`3.14`, `0.5`, `-1.0`
`bool`	Booleans	`true`, `false`
`string`	Strings	`"hello"`, `""`
`char`	Characters	`'a'`, `'z'`
`unit`	The unit type	`()`

Arbitrary precision

IML integers and reals have arbitrary precision — there are no overflow or rounding issues. The int type corresponds to mathematical integers (ℤ), and real corresponds to the algebraic reals. You can only write rational constants as members of the type, but all reasoning treats them as algebraic reals. This is sound and complete for real reasoning modulo polynomial constraints due to quantifier elimination over the theory of real closed fields (RCF).

Arithmetic

Integer arithmetic works as you'd expect:

let sum = 3 + 4          (* 7 *)
let diff = 10 - 3        (* 7 *)
let prod = 6 * 7         (* 42 *)
let quot = 17 / 5         (* 3 — integer division *)
let rem = 17 mod 5        (* 2 *)

Real arithmetic uses the same operators:

let x = 1.5 + 2.5        (* 4.0 *)
let y = 3.0 * 2.0        (* 6.0 *)
let z = 7.0 / 2.0        (* 3.5 *)

Comparison operators work on both integers and reals:

let a = 3 < 4             (* true *)
let b = 3 >= 3            (* true *)
let c = 5 = 5             (* true — structural equality *)
let d = 5 <> 6            (* true — inequality *)

Boolean operators

let a = true && false     (* false — logical AND *)
let b = true || false     (* true — logical OR *)
let c = not true          (* false — logical NOT *)

In logical contexts (theorems, verification goals), you also have:

(* Implication: if p then q *)
let implies p q = p ==> q
 
(* Biconditional: p if and only if q *)
let iff p q = (p ==> q) && (q ==> p)

Conditionals

Use if/then/else for conditional expressions:

let abs x =
  if x >= 0 then x else -x
 
let max a b =
  if a >= b then a else b
 
let classify n =
  if n > 0 then "positive"
  else if n < 0 then "negative"
  else "zero"

Both branches required

In IML, if/then expressions always require an else branch. This is because every expression must have a well-defined value — there's no concept of "doing nothing."

Let bindings and scope

let can introduce local bindings with in:

let hypotenuse a b =
  let a_sq = a * a in
  let b_sq = b * b in
  Int.sqrt (a_sq + b_sq)

Multiple bindings can be introduced sequentially:

let compute x =
  let y = x + 1 in
  let z = y * 2 in
  z + y

Tuples

Tuples group multiple values together:

let pair = (1, 2)
let triple = ("hello", 42, true)
 
(* Destructuring *)
let (a, b) = pair
let sum_pair (x, y) = x + y

Lists

Lists are one of IML's most important data structures:

let empty = []
let nums = [1; 2; 3; 4; 5]
let words = ["hello"; "world"]
 
(* Cons operator *)
let more_nums = 0 :: nums    (* [0; 1; 2; 3; 4; 5] *)
 
(* Append *)
let combined = [1; 2] @ [3; 4]  (* [1; 2; 3; 4] *)

Lists are the primary recursive data structure in IML, and many of ImandraX's most impressive proofs involve reasoning about list-manipulating functions.

Options

The option type represents values that may or may not exist:

let found = Some 42
let missing = None
 
let describe = function
  | Some x -> "found: " ^ string_of_int x
  | None -> "not found"

Type annotations

IML has powerful type inference, but you can add explicit annotations:

let x : int = 42
let f (x : int) : bool = x > 0
let g (xs : int list) = List.length xs

Type annotations are sometimes required for [@@opaque] functions and can improve error messages.

Comments

(* This is a single-line comment *)
 
(* This is a
   multi-line comment *)
 
(* Comments can be (* nested *) *)

Evaluation

You can evaluate expressions directly using eval:

eval 2 + 3              (* 5 *)
eval List.rev [1; 2; 3] (* [3; 2; 1] *)
eval List.length [1; 2; 3; 4; 5]  (* 5 *)

This is useful for testing and exploring functions before proving properties about them.