Split Decidable goal

Stream: lean4

[Chris B]

Is there a way to use split when the goal is an instance of decidable? Naively invoking split with the goal below gives me the error tactic 'split' failed:

  Decidable
    (match (x, y) with
    | (ctor s₁, ctor s₂) => ¬s₁ = s₂
    | x => False)

[James Gallicchio]

is this thread potentially related?

[Leonardo de Moura]

@Chris B split was originally written to synthesize proofs, not code. I just pushed a commit that removes this restriction. The generated code for your example looks reasonable. I added your example to the test suite.
https://github.com/leanprover/lean4/commit/2fc23a2a2b3d61e917d41de504577156d01ee227

[Leonardo de Moura]

BTW, I still have to improve the split error message. It is not very informative.

[Chris B]

Thank you!