inductive type <-> disjunction of constructors

Stream: general

[Hunter Freyer]

Let's say I have a type family like this:

inductive typed : fn2 -> val -> val -> Prop
| zero : typed fn2.zero val.nil val.nat
| succ : typed fn2.succ val.nat val.nat
....

There's only the one constructor that has fn2.zero in the first argument position. I'm trying to prove decidable (typed fn2.zero a b). I feel like the easiest thing is to convert this to decidable ((a = val.nil) /\ (b = val.nat)). Is there a way to do that? To convert an inductive type into an "or" over all its constructors?

[Hunter Freyer]

(I could do case splits as well, of course, but the more complex the constructors get, the harder it is to just split on everything)

[Yury G. Kudryashov]

See https://leanprover-community.github.io/mathlib_docs/commands.html#mk_iff_of_inductive_prop

[Yury G. Kudryashov]

BTW, does @[derive decidable] work?

[Mario Carneiro]

no

[Hunter Freyer]

Can anyone give an example of how to use mk_iff_of_inductive_prop?

[Hunter Freyer]

I think I got it: run_cmd tactic.mk_iff_of_inductive_prop `typed `typed_iff

[Simon Hudon]

Or you can do

mk_iff_of_inductive_prop typed typed_iff

as a declaration

[Simon Hudon]

I think it would fit in better as an attribute though

[Hunter Freyer]

aye. Thanks!