小编pki*_*pki的帖子

我想以某种方式限制允许构造函数在归纳定义中采用何种类型的输入.我想说如下定义二进制数:

Inductive bin : Type :=
  | O : bin
  | D : bin -> bin
  | S : bin -> bin.

这里的想法是D通过在末尾添加零来使非零数字加倍,并且S将数字作为最后一位数加零,并将最后一位数字变为一位.这意味着以下是合法数字:

S 0
D (S 0)
D (D (S 0))

而以下不是:

S (S 0)
D 0

有没有办法以干净的方式在归纳定义中强制执行这些限制？