## Stream: general

### Topic: inductive type <-> disjunction of constructors

#### Hunter Freyer (Oct 03 2020 at 01:18):

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 (Oct 03 2020 at 01:19):

(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 (Oct 03 2020 at 01:44):

BTW, does @[derive decidable] work?

no

#### Hunter Freyer (Oct 03 2020 at 14:11):

Can anyone give an example of how to use mk_iff_of_inductive_prop?

#### Hunter Freyer (Oct 03 2020 at 14:15):

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

#### Simon Hudon (Oct 03 2020 at 14:30):

Or you can do

mk_iff_of_inductive_prop typed typed_iff


as a declaration

#### Simon Hudon (Oct 03 2020 at 14:30):

I think it would fit in better as an attribute though

#### Hunter Freyer (Oct 03 2020 at 14:38):

aye. Thanks!

Last updated: May 09 2021 at 19:11 UTC