Lean4新手编写素数判断函数遭遇lake build编译合成错误求助

错误原因分析 #

你的代码出现编译错误核心问题如下：

• 类型名称错误：Lean4中自然数类型是大写Nat，你使用了小写nat，导致编译器无法找到Nat对应的算术操作实例（如乘法HMul、取模HMod、数字字面量OfNat）。
• 表达式优先级问题：递归调用isPrimeF x i+1 v里，i+1未加括号，Lean会错误解析为(isPrimeF x i) + 1 v，属于非法函数调用格式。
• 递归终止性缺失：Lean4要求递归函数必须能被证明终止，这里可通过partial关键字快速跳过终止性检查（该函数中i从2递增到√x，必然终止）。
• 边界情况未处理：未对小于等于1的数字做特殊判断，会导致无效递归。

修正后的代码 #

partial def isPrimeF (x : Nat) (i : Nat) (v : Bool) : Bool :=
  if i*i == x then v
  else
    match x % i with
    | 0 => false
    | _ => isPrimeF x (i+1) v

def isPrime (x : Nat) : Bool :=
  if x ≤ 1 then false
  else isPrimeF x 2 true

#eval isPrime 12  -- 输出：false
#eval isPrime 13  -- 输出：true
#eval isPrime 27  -- 输出：false
#eval isPrime 29  -- 输出：true

关键修正点说明 #

1. 类型修正：将所有nat替换为Nat，让编译器正确识别自然数类型的算术操作。
2. 括号调整：把isPrimeF x i+1 v改为isPrimeF x (i+1) v，确保i+1作为完整参数传递。
3. 添加partial关键字：标记isPrimeF为部分函数，跳过Lean4的终止性检查，快速验证功能。
4. 边界处理：在isPrime中增加x ≤ 1的判断，直接返回false，避免无效递归。
5. 求值命令修正：移除#eval!的感叹号，使用Lean4标准的#eval命令。

内容的提问来源于stack exchange，提问作者Mouedh Souabni