Subject: Ssreflect Users Discussion List
List archive
- From: bertot <>
- To: ssreflect <>
- Subject: [ssreflect] Question of style
- Date: Tue, 05 Nov 2013 15:11:53 +0100
Hello,
I am using poly.v and I need to reduce
- 'X \Po p
into -p
It seems that there is a theorem missing, with name
comp_poly_opp and statement
-p \Po q = -(p \Po q)
or something semantically equivalent. Do you agree?
Yves
- [ssreflect] Question of style, bertot, 11/05/2013
- Re: [ssreflect] Question of style, Laurent Théry, 11/05/2013
- RE: [ssreflect] Question of style, Georges Gonthier, 11/05/2013
Archive powered by MHonArc 2.6.18.