Синтаксис Coq для определения лемм

Question

Я вижу другой синтаксис Coq для определения лемм.Например, Lemma plus_n_O: forall n:nat, n = n + 0. и Lemma plus_n_O n: n = n + 0. оба определяют, что сумма нуля по любому числу равна числу.Чем отличаются эти определения?Или это новая функция Coq для удаления квантификатора forall из определений.

Answer 1

Эти два определения по существу эквивалентны. Вообще говоря, любое утверждение вида

Lemma foo x y z : P.
Proof.
(* ... *)

эквивалентно

Lemma foo : forall x y z, P.
Proof.
intros x y z.
(* ... *)