Могу ли я использовать функции в Coq в качестве конструкторов?

Question

Я пытаюсь написать функцию, чтобы определить, является ли число нечетным, и вернуть его, если оно есть, а не, если это не так. Чтобы сделать это, я сопоставил число с нечетной функцией, которая возвращает true, если оно нечетное. Как я могу использовать это как конструктор? введите описание изображения здесь

Answer 1

Вы не можете использовать любую функцию, как если бы она была конструктором в предложении match. Только конструкторы, которые появляются в объявлении типа данных, могут быть использованы таким образом. Тем не менее, функция oddb возвращает логическое значение, которое является типом данных, определенным конструкторами, и, таким образом, вы можете сопоставить его результат:

match oddb n with
| true  => (* return something *)
| false => (* return something else *)
end

Вы можете написать эту более подробную форму в виде регулярное выражение if-then-else, встречающееся в других функциональных языках программирования. Когда вы пишете

if oddb n then
  (* return something *)
else 
  (* return something else *)

Coq автоматически переводит ваш ввод в форму выше.