Take the 2-minute tour ×  I would like to somehow limit what
kind of inputs constructors are allowed to take in an inductive
definition. Say I want to say define binary numbers as follows:
Inductive bin : Type :=   | O : bin   | D : bin -> bin   | S :
bin -> bin.  The idea here is that D doubles up a nonzero number
by adding a zero at the end and S takes a number with zero as
the last digit and turns the last digit into a one. This means
that the following are legal numbers:  S 0 D (S 0) D (D (S 0))
while the following would not be:  S (S 0) D 0  Is there a way
to enforce such restrictions in an inductive definition in a
clean way?  share|improve this question add comment  2 Answers
up vote 6 down vote accepted  You could define what it means for
a bin to be legal with a predicate, and then give a name to the
subset of bins that obey that predicate. Then you write
functions with Program Definition and Program Fixpoint instead
of Definition and Fixpoint. For recursive functions you'll also
need a measure to