function definitions with ↦

Stream: lean4

[Paul Chisholm]

I notice that recently ↦ was added to allow use in anonymous functions instead of =>. However, it is not possible to use it when functions are defined with matches. The following are accepted:

def f : Nat → Nat := fun x ↦ x
def f' : Nat → Nat := fun x => x
def g' : Nat → Nat | x => x

but the following is flagged as invalid

def g : Nat → Nat | x ↦ x

Is this a deliberate decision, or are there plans to extend the use of ↦?

[Horațiu Cheval]

I guess it's deliberate. Relevant discussion regarding the introduction of ↦: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.3D.3E.20notation