Modules & Imports

ImandraX supports a module system and a path-based import system for organizing code across multiple files.

Modules

Modules group related definitions together:

module Geometry = struct
  type point = { x : real; y : real }
 
  let origin = { x = 0.0; y = 0.0 }
 
  let distance p1 p2 =
    Real.sqrt Real.((p1.x - p2.x) * (p1.x - p2.x) +
                     (p1.y - p2.y) * (p1.y - p2.y))
end

Access module contents with dot notation:

let p = Geometry.{ x = 3.0; y = 4.0 }
let d = Geometry.distance Geometry.origin p

Or open the module to bring its contents into scope:

open Geometry
let d = distance origin { x = 3.0; y = 4.0 }

The import system

ImandraX uses [@@@import] directives to bring definitions from other .iml files into scope:

(* Import everything from utils.iml *)
[@@@import "utils.iml"]
 
(* Import a file and bind it to a module name *)
[@@@import MyUtils, "utils.iml"]
 
(* Then access via the module name *)
let x = MyUtils.helper_function 42

Import paths

Import paths are resolved relative to the current file's directory:

(* Same directory *)
[@@@import "helpers.iml"]
 
(* Subdirectory *)
[@@@import "lib/math.iml"]
 
(* Parent directory *)
[@@@import "../common/types.iml"]

Selective opening

After importing with a module name, you can selectively open it:

[@@@import Math, "math.iml"]
 
(* Open specific submodules *)
open Math.Theorems
open Math.Types

Multi-file projects

For larger projects, organize your code across multiple files with clear dependency structure:

my-project/
├── types.iml          (* Shared type definitions *)
├── utils.iml          (* Helper functions and lemmas *)
├── core.iml           (* Core logic, imports types.iml and utils.iml *)
├── properties.iml     (* Theorems about core, imports core.iml *)
└── mod.iml            (* Optional: module re-exports *)

A mod.iml file can serve as a module index, re-exporting definitions:

(* mod.iml *)
[@@@import Types, "types.iml"]
[@@@import Utils, "utils.iml"]
[@@@import Core, "core.iml"]

Example: The 100 Theorems project

The ImandraX 100 Theorems project uses this pattern:

(* sqrt2_irrational.iml *)
[@@@import "mod.iml"]
[@@@import GCD, "gcd.iml"]
 
open Mod.Theorems
open GCD
 
(* ... proof definitions ... *)

ImandraX tracks dependencies between files. When you modify a file, only files that depend on it (directly or transitively) are re-checked. This is handled automatically by both the VS Code extension and the CLI.

Differences from Imandra Core

ImandraX's import system replaces the older use, mod_use, import, and require directives from Imandra Core with the unified [@@@import] syntax. See Differences from Imandra Core for details.