Unicode symbol for function arrow

[phlegmaticprogrammer]

Right now an anonymous ProofScript function is written like

x => x * x

or, using prettier Unicode

x ⇒ x * x

It would be better for the pretty version to look like this

x ↦ x * x

[phlegmaticprogrammer]

It is OK to write anonymous functions in scripts either like that:

x => x * x

or like that:

x ↦ x * x

Note that for case expressions, you still write them either like that:

match y
  case x => x * x

or like that:

match y
  case x ⇒ x * x