Partial def versus def

Stream: lean4

[Siddharth Bhat]

I imagined that a partial def will succeed whenever a def would. However, this example shows that this is not the case:

inductive TestResult
| success
| failure (err: String)

class Shrinkable (α : Type) where
  shrink: α → List α

partial def minimizeCounterexample [Shrinkable α] (a: α) (p: α -> TestResult): α × String :=
  let rec go (xs: List α): α × String:=
    match xs with
    | [] =>
      match p a with
      | TestResult.success => (a, "ERROR: MINIMAL COUNTEREXAMPLE SUCCEEDED ON INPUT")
      | TestResult.failure err => (a, err)
    | x::xs => go xs
  go (Shrinkable.shrink a)

The partial def errors with:

10:0: error: failed to compile partial definition 'minimizeCounterexample.go',
failed to show that type is inhabited

while the file type checks with a def. I imagine this is because Lean doesn't attempt to verify if the partial def is well-founded, and simply tries to create an inhabitant for proof-theoretic concerns? Is it possible to change this to have Lean check if a partial def would succeed as a def? I am unsure if the overhead is worth it, however.

[Mac]

@Siddharth Bhat as with a constant you need to show that the result of a partial def is Inhabited (to prevent i from potentially rendering Lean's logic unsound). In your example, this can be done by simply adding [Inhabited α] to the function's signature.