Zulip Chat Archive

Stream: general

Topic: How to indicate empty matches in Lean 4


view this post on Zulip François G. Dorais (Jan 05 2021 at 11:22):

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.

view this post on Zulip Notification Bot (Jan 05 2021 at 12:02):

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


Last updated: May 10 2021 at 00:31 UTC