如何在固定点定义代码中创建条件

Question

我正在阅读“软件基础”这本书，并且正在研究第二章中的最后一个问题。该问题要求将自然数转换为二进制数，其中二进制数的定义方式如下：

  - [is] zero,
  - [is] twice a binary number, or
  - [is] one more than twice a binary number.

我的思维过程是，如果一个自然数是偶数，那么它可以表示为

double(nat_to_bin n)

然而，在我的Fixpoint定义中，当我试图编写

(evenb n' = true) => double(nat_to_bin)

我收到一个错误，因为evenb n‘不是nat的构造函数。有没有办法在不改变nat定义的情况下，创建一个条件，使上面的行成为有效的函数定义？

Answer 1

算了，我想出了一个解决方案。我可以直接写下这个词

match (evenb n') with
| true => ....

不过，我还是花了一段时间。