编辑“︁Lean与OCaml交互”︁（章节）

== 在Lean中调用OCaml代码 ==  

Lean提供了`foreign`关键字和`@[extern]`属性，允许开发者声明OCaml函数并在Lean中调用它们。以下是一个简单的示例：

<syntaxhighlight lang="lean">
-- 声明一个OCaml函数，该函数接收两个整数并返回它们的和
@[extern "ocaml_add"]
def ocamlAdd (a b : Nat) : Nat :=
  a + b  -- 这里的实现仅用于类型检查，实际调用时会跳转到OCaml代码

-- 调用OCaml函数
#eval ocamlAdd 3 5  -- 输出: 8
</syntaxhighlight>

对应的OCaml实现（假设编译为动态库`ocaml_add.so`）：  
<syntaxhighlight lang="ocaml">
let ocaml_add a b = a + b
</syntaxhighlight>

=== 详细步骤 ===  
1. **编写OCaml代码**：将OCaml函数编译为动态库（如`.so`或`.dll`）。  
2. **在Lean中声明外部函数**：使用`@[extern]`属性标记Lean函数，并指定OCaml函数名。  
3. **加载动态库**：在运行Lean时，确保动态库位于系统库路径中。