Я работаю над книгой «Основы программного обеспечения», и у меня возникла последняя проблема во второй главе.Проблема состоит в том, чтобы преобразовать натуральное число в двоичное число, где двоичное число определяется следующими способами:
- [is] zero,
- [is] twice a binary number, or
- [is] one more than twice a binary number.
Мой мыслительный процесс заключается в том, что если натуральное число четное, то оно может быть выраженоas
double(nat_to_bin n)
Однако, в моем определении Fixpoint, когда я пытался написать
(evenb n' = true) => double(nat_to_bin)
, я получил ошибку, потому что evenb n 'не является конструктором nat.Можно ли как-нибудь создать условное выражение так, чтобы приведенная выше строка была корректным определением функции без изменения определения nat?