E0039

Warning name: missing_reasoning

错误案例

循环缺少 proof_reasoning 子句。

///|
fn fib(n : Int) -> UInt64 {
  for i = 0, a = 0UL, b = 1UL; i < n; i = i + 1, a = b, b = a + b {

  } else {
    b
  }
}

建议

添加一些证明推理。

///|
fn fib(n : Int) -> UInt64 {
  for i = 0, a = 0UL, b = 1UL; i < n; i = i + 1, a = b, b = a + b {

  } nobreak {
    b
  } where {
    proof_reasoning: (
      #|The variables `a` and `b` represent consecutive Fibonacci numbers, 
      #|so `a` is always less than or equal to `b`.
      #|
    ),
  }
}