search

math-comp / mcb

Mathematical Components (the Book)
Other
139 stars 25 forks source link

Definition of ex2 on 4.2.1 #106

Open gaxiiiiiiiiiiii opened 3 years ago

gaxiiiiiiiiiiii commented 3 years ago

The book saids:

Inductive ex2 A P Q : Prop := ex_intro2 x of P x & Q x.

I guess it should be like this:

Inductive ex2 A P Q : Prop := ex_intro2 (x : A) of P x & Q x.