The Coq mailing list

["" <judy AT mail.ccnu.edu.cn>]

Dear Mr.COQ

I am a beginner of studying COQ,and I've found it is realy hard to learn.

I have some questions about the proof of the proposition A->B->B/\A ,here 
from the
value table we found that it is not an always true proposition if the 
notation"->"
here means imply as a propositional connective.

so what does the notation"->" realy mearn ??
Does it only mean that the proposition before "->"can only be true??

A B  A->B B/\A  A->B->B/\A 
1 1   1    1    1           
1 0   0    0    1           
0 1   1    0    0           
0 0   1    0    0


sincerely  Judy
MSN:judy2250 AT hotmail.com