Understanding partial

Stream: lean4

[Marcus Rossel]

Why does this work?:

partial def part (x : Nat) : Nat := part x
def safe (x : Nat) := part x -- This doesn't have to be marked as partial?

I was expecting safe to be required to be marked as partial as well, as it calls a partial function.

[Henrik Böving]

What you are talking about would be the behaviour ofunsafe (which is what partial uses under the hood) The Lean 4 manual states:
When the partial keyword is used, Lean generates an auxiliary unsafe definition that uses general recursion, and then defines an opaque constant that is implemented by this auxiliary definition.

Meaning that partial desugars to an unsafe def and a constant which is marked with an @implementedBy attribute pointing to the unsafe implementation and is thus logically sound (since constant types have to be inhabited).