matching on `Char.ofNat`

Stream: lean4

[Jovan Gerbscheid]

I noticed that Char.ofNat is tagged as @[match_pattern], but if I actually try to match on it, I get an error:

#check match ' ' with
  | .ofNat 5 => true
  | _ => false

gives the error

tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'Or.casesOn' can only eliminate into Prop
case mk.mk.mk.case_1
motive: Char → Sort ?u.2602
h_1: Unit →
  motive
    { val := { val := { val := 5, isLt := (_ : 5 < UInt32.size) } },
      valid := (_ : 5 < 55296 ∨ 57343 < 5 ∧ 5 < 1114112) }
h_2: (x : Char) → motive x
isLt✝: 5 < UInt32.size
valid✝: UInt32.isValidChar { val := { val := 5, isLt := isLt✝ } }
⊢ motive { val := { val := { val := 5, isLt := isLt✝ } }, valid := valid✝ }
 after processing
  (Char.mk (UInt32.mk (@Fin.mk 5 _)) _)
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil