элементы группы с ограничениями
Часть причин, по которым они не находятся в той же области, состоит в том, что в любой точке блока try вы можете исключить исключение. Если они были в одном и том же объеме, это была катастрофа в ожидании, потому что в зависимости от того, где было выбрано исключение, это может быть еще более неоднозначным.
По крайней мере, когда объявлено за пределами блока try, вы знаете наверняка, какая переменная могла бы быть минимальной, когда генерируется исключение; Значение переменной перед блоком try.
1 ответ
По-видимому, вы предполагаете, что существует такая вещь, как функция div. В голом Coq, без загруженной библиотеки, такой функции не существует.
Чтобы иметь функцию, которая выглядит как деление натуральных чисел, я предлагаю вам загрузить библиотеку Arith. Тогда вам будет разрешено использовать обозначение a / b для деления.
Вот пример:
Require Import Arith.
Check (fun x y => x / y).
(* this returns : fun x y : nat => x / y : nat -> nat -> nat *)
Compute (12 / 5).
(* this returns : = 2 : nat *)
Locate "_ / _".
(* this returns : "x / y" := Nat.div x y : nat_scope *)
Я до сих пор не понимаю, что вы подразумеваете под минимумом и максимумом группы, но, по крайней мере, вы сможете написать некоторый код Coq, который будет принят по системе.