模块系统

目录即模块

一个目录 = 一个模块。项目里每个子目录默认是一个独立模块。

MY_PROJECT/
  main.subl                ← 根模块（有全局唯一 main()）
  MY_PROJECT.settings      ← 根模块声明（mount 依赖）
  stdlib/                  ← 标准库（隐式自动挂载，无需声明）
  users/                   ← 子模块目录
    users.subl
    users.settings

挂载 mount

在 .settings 文件里用 mount 声明依赖：

# MY_PROJECT.settings
mount users
mount stdlib

• stdlib/（根目录下）隐式自动挂载——任何模块都能直接用。
• 挂载后，被挂载模块里的类型、函数、构造子、定理对当前模块可见。

跨模块解析

裸名自动跨模块解析：

// 本模块没有定义 Ok/Err，但 stdlib/collection 有——直接可用
var r: Result[Nat, Str] = Ok(42)

构造子（如 Ok/Err）、结构体、函数、定理都会在可见模块（含 stdlib）里依次查找。

定理跨模块搜索

证明时，定理搜索沿可见路径跨模块展开：

+∵ n ∈ (0..30)
∴ n ≥ 0            // 命中 stdlib/logic.subl 的 rangeLowerBound / natNonNeg

编译

java -jar sublimation.jar compile MY_PROJECT -o out.js
node out.js

用目录路径作为编译入口（而非单个文件），即走模块系统。