inverse of simple function

Stream: lean4

[Locria Cyber]

inductive Tile where
| empty
| wall
| player
| target
| box
deriving Inhabited


def Tile.toChar : Tile -> Char
| .wall => '#'
| .empty => ' '
| .target => '.'
| .player => '@'
| .box => 'o'

def Tile.parseP? : (c: Char) -> Option {t: Tile // c = t.toChar}
| '#' => .some ⟨.wall,   (by simp)⟩
| ' ' => .some ⟨.empty,  (by simp)⟩
| '.' => .some ⟨.target, (by simp)⟩
| '@' => .some ⟨.player, (by simp)⟩
| 'o' => .some ⟨.box,    (by simp)⟩
| other => .none

[Locria Cyber]

Is there a shorter way to write Tile.parseP?? Like using reflection

[Kevin Buzzard]

When you've finished sokoban can you do nethack?

[Marcus Rossel]

I guess you could do (untested):

def Tile.all := [empty, wall, player, target, box]

def Tile.parseP? (c : Char) : Option { t : Tile // c = t.toChar } :=
  Tile.all.findSome? fun t =>
    if h : c = t.toChar
    then some { val := t, property := h }
    else none

But that's gonna be slower than your version.