Example for "inaccessible patterns" is not really helpful?

I am trying to understand how inaccessible patterns work, and I was hoping the given example would help:

https://github.com/leanprover/reference-manual/blob/b00d397cf2efed105cb441b737b583b3a83f2c74/Manual/Terms.lean#L1279-L1282

It doesn't.

AFAICT, the use of the inaccessible pattern in this example is not necessary. It seems to work fine if I just remove it:

def half' (n : Nat) : Nat :=
  match n.parity with
  | .even h => h
  | .odd h  => h

When I do #print half', I see that the compiler indeed rewrites it using the inaccessible pattern notation (as in the original implementation), but this doesn't really help my understanding (even if that would have been mentioned in the manual).

Can this example please be replaced by one that actually needs to use an inaccessible pattern (i.e. it wouldn't work without it)?
I would hope to get a bit more explanatory power out of it ...

If the example cannot be changed, it would at least probably help a little bit to mention that the compiler adds the inaccessible pattern automatically when possible (or whatever the rules are for that).

Start at Manual/Terms.lean around lines 1279-1282 and compare the current inaccessible-pattern example with the reported version without the pattern. Replace it with an example that genuinely requires inaccessible-pattern notation, or clarify in the surrounding text when the compiler inserts that notation automatically. Done means the manual example provides explanatory value and matches the documented behavior.