Меньше, чем функция - PullRequest
Новая
       71

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

0 голосов
/ 31 декабря 2018

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

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

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

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

1 Ответ

0 голосов
/ 01 января 2019

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

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