Как я могу разыграть нат в int в Изабель - PullRequest
Новая
       21

Как я могу разыграть нат в int в Изабель

1 голос
/ 02 ноября 2019

Выполняя домашнее задание, я застрял в следующем вопросе:

Создать функцию add. Возвращает сумму двух натуральных чисел. Докажите, что это работает.

Я застрял, потому что, чтобы написать код, чтобы доказать это, мне нужно привести натуральное число (nat в Изабель) к int.

Вот функция add, которую я написал: 

primrec add :: "nat ⇒ nat ⇒ nat"
  where
    add01: "add x 0 = x" |
    add02: "add x (Suc y) = Suc (add x y) "

Чтобы узнать результат, я сделал это: 

value "somaNat (Suc(Suc(0))) (Suc(0))"

Возвращает 3, как и должно. 

Suc(Suc(0) = 2
Suc(0) = 1

Также попытался создать функцию, которая преобразует ее в int, например: 

primrec nat_to_int :: "nat ⇒ int"
  where
  nat_to_int02: "nat_to_int x = value x"

Не работает, потому что (value x) не может быть справа.

Я искал его в учебнике, который предоставляет Изабель, и в другом, который нашел в Интернете.

Самый близкий вопрос, который я нашел на SO, был такой: Приведение int к nat вИзабель

Итак, как я могу разыграть nat в int в Изабель?

...