Zulip Chat Archive

Stream: new members

Topic: Eliminating on decidable equality

Oskar Berndal (Dec 28 2020 at 17:38):

Hi! I'm trying to define a Syntax (with dB indices). As part of that I want to define substitution. This however requires me to eliminate on whether two variables (integers) are equal. I tried to define a Term of Syntax by doing

cases (decidable.em (x = major)),

where x and major are nats in the context. But it says that 'induction tactic failed, recursor 'or.dcases_on' can only eliminate into Prop. I want to ask, how can I eliminate on the decidability of equality of nats such that I can define a term of any type? Thanks! =)

Johan Commelin (Dec 28 2020 at 17:45):

@Oskar Berndal Do you just want

if x = major then foo else bar

Oskar Berndal (Dec 28 2020 at 17:48):

Oh yes I believe I do. Thanks! =)

Mario Carneiro (Dec 28 2020 at 18:22):

you can also use by_cases x = major in tactic mode

Last updated: Dec 20 2023 at 11:08 UTC