Example for "inaccessible patterns" is not really helpful?

[mgeier]

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

reference-manual/Manual/Terms.lean

Lines 1279 to 1282 in b00d397

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

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).