Меньше, чем функция

Question

Я прохожу курс обучения "Логические основы". Решение проблемы:

Имея меньшую или равную функцию:

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => leb n' m'
      end
  end.

создать функцию "меньше":

Definition blt_nat (n m : nat) : bool
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Насколько я понимаю, это должно работать так:

if (n == m)
   return false
else
    return (leb n m)

Я создал это:

Definition blt_nat (n m : nat) : bool
  match n with
  | m => false
  | _ => leb n m
  end.

Но это не работает - выводит: "Ошибка: это предложение является избыточным". для линии:

| _ => leb n m

Пожалуйста помоги.

Answer 1

Используя match ... with...endмы можем просто проверить конструкторы определенного типа данных и выяснить, как он построен на основе своих конструкторов. Таким образом, вы не можете сопоставить тип данных nat с другим типом данных nat. Вы можете найти другие примеры здесь.

Definition blt_nat (n m : nat) : bool :=
  match m with
  | 0 => false
  | S m' => leb n m'
  end.