The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

Hi all!

Let's take the following inductive type (simplified example):

Inductive Op :=
  |  add (_:nat)  : Op
  |  remove  :  Op
  |  replace  (_:nat)  :  Op.

I want to write a partial function which can take only an 'add' or
'replace' operation and returns a value of type T. I've found (at
least) three ways of specifying it:

Definition do_stuff (a: Op) : T + { a = remove }.
  ... Defined.

Definition do_stuff' (a: Op) : (a <> remove) -> T.
  ... Defined.

Definition do_stuff'' (a: {o: Op | o <> remove}) : T.
  ... Defined.

I believe all three are equivalent. Do you agree?

I'm trying to decide which to go ahead with. In your experience, what
are the advantages and disadvantages of each of these choices in
practice? Which do you prefer?

Thanks!

--
www.mhelvens.net