CODEWITHSUNDEEP
coq
Jennifer L
Jennifer L

Reputation: 156

Coq syntax for defining lemmas

I can see the different syntax of Coq for defining lemmas. For example, Lemma plus_n_O: forall n:nat, n = n + 0. and Lemma plus_n_O n: n = n + 0. both define that the sum of zero by any number is equal to the number. How these definitions differ? Or this is a new feature of Coq to remove forall quantifier from definitions.

Upvotes: 2

Views: 112

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

These two definitions are essentially equivalent. Generally speaking, any statement of the form

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

is equivalent to

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

Upvotes: 3

Related Questions