partial_fixpoint: failed to generate equational theorem

[nomeata]

David pointed out this bug to me:

def find42 : Nat → Bool
  | 42 => true
  | n => find42 (n + 1)
partial_fixpoint

/--
error: failed to generate equational theorem for 'find42'
x : Nat
x_1 : x = 42 → False
⊢ (match x with
    | 42 => true
    | n =>
      Lean.Order.fix
        (fun f x =>
          match x with
          | 42 => true
          | n => f (n + 1))
        find42.proof_3 (n + 1)) =
    find42 (x + 1)
-/
#guard_msgs in
#print equations find42

Versions

Lean 4.16.0-nightly-2025-01-27

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.