mapsto in case tactic not allowed

Stream: new members

[Matthew Pocock]

I'm working through chapter 5.

theorem test_structured (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
  apply And.intro
  case left ↦ exact hp
  case right ↦ exact And.intro hq hp

This fails. It requires the ascii => in this place. Seems inconsistent with lambdas where the mapsto symbol is accepted. I am on "4.0.0-nightly-2023-09-01".

[Eric Wieser]

This has never worked, but it has been discussed before. If you wrote that following instructions somewhere, then I guess those instructions need fixing

[Matthew Pocock]

Eric Wieser said:

This has never worked, but it has been discussed before. If you wrote that following instructions somewhere, then I guess those instructions need fixing

No, I wasn't following instructions. I was just assuming it would work here because it worked elsewhere for the same symbol.

[Kevin Buzzard]

This is indeed a reasonable assumption and it's a shame it doesn't work in this case.

[Patrick Massot]

I never understood why maps to isn't allowed everywhere => is allowed.

[Kevin Buzzard]

Right -- mathematicians are using mapsto in the same way that they use other unicode (i.e. all over the place) whereas the computer scientists are spelling it out in ascii and using font hacks. I am still very unclear why this is such a contentious issue.

[Eric Wieser]

Mario Carneiro said:

mapsto only makes sense for functions IMO

[Kevin Buzzard]

"case left maps to exact hp" sounds fine to me.

[Eric Wieser]

Another old relevant message:

Kyle Miller said:

Here's a proposal:

• Allow using => or ⇒ interchangably, just like how we already allow ->or →
• For functions (terms) we use ↦, everywhere else (structural constructs) we use => or ⇒.

(Unfortunately ⇒ looks really silly in VS Code with the default font... Looks fine here though.)

Anyway, this is a color I'd be happy with for my bike shed :bicycle: