Default argument in match pattern

Stream: lean4

[Siddharth Bhat]

Consider the MWE:

inductive Foo
| mk : Int → Foo

@[match_pattern]
def foo0Default (val : Int := 0) : Foo := Foo.mk val

def Foo.toBool : Foo → Bool
| foo0Default => True -- explicit parameter is missing, unused named arguments []
| _ => False

I would have expected the match to go through, with foo0Default being the same as foo0Default 0