mcb icon indicating copy to clipboard operation
mcb copied to clipboard

Published 20 hours ago • verified publisher icon math-comp

Definition of ex2 on 4.2.1

Open gaxiiiiiiiiiiii opened this issue 4 years ago • 0 comments

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.

gaxiiiiiiiiiiii avatar Dec 14 '20 11:12 gaxiiiiiiiiiiii