How to indicate empty matches in Lean 4

Stream: general

[François G. Dorais]

In Lean 3, a period can be used to indicate an empty match:

inductive test : bool → Type | of_tt : test tt

def test_ff_is_empty : test ff → empty .

Is there a similar thing in Lean 4? I can make it work using tactic mode:

inductive Test : Bool → Type | ofTrue : Test true

def testFalseIsEmpty : Test false → Empty := by {intro x; cases x}

Since Test has a parameter, using recursors directly is a major pain. Nothing else I tried seems to work.

[Notification Bot]

This topic was moved by Rob Lewis to #lean4 > How to indicate empty matches in Lean 4