negation of earlier cases of match

Stream: general

[Nima]

(deleted)

[Nima]

How should I change the following code, so in the second case I know a is not aa?

inductive ind | aa | bb
open ind
example : ind → ind → ind → ind → nat
| aa _  _ _ := 0
| a  aa _ _ := sorry
| _  _  _ _ := 0

[Kenny Lau]

you can change the title next time

[Kenny Lau]

type bb instead of a

[Kenny Lau]

(it can't know inside a match what conditions are not yet matched)

[Nima]

How do I change the title?
what if I have
inductive ind | aa | bb | cc | dd

[Kenny Lau]

maybe could you give us the whole context? I sense some XY problem going on here

[Kenny Lau]

sorry

[Johan Commelin]

How do I change the title?

Just edit the post. There will be a field to edit the title as well.

[Simon Hudon]

what if I have
inductive ind | aa | bb | cc | dd

I think you'd need an if _ then _ else _ and a match inside one of the branches

[Kenny Lau]

ite is hard to destruct. I don't recommend using it at all unless necessary

[Kenny Lau]

I'm sure his situation has other ways out

[Simon Hudon]

It would help if you derived decidable_eq:

@[derive decidable_eq]
inductive ind | aa | bb | cc | dd

[Simon Hudon]

Kenny, the alternative would be to match on all branches.

[Kenny Lau]

one can't be so sure

[Nima]

So if I have a sparse match on many variables, and in each case I want to use the fact that previous cases were not a match, I would be better off with if-then-else. Right?

[Simon Hudon]

Exactly

[Nima]

Thanks