You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Just a minor remark : QuantumLib.Complex.Cconj_opp uses a variable named capitalized C, which is unfortunate, since C is here the type of the complex numbers. Even if that doesn't prevent from using this lemma, could you rename this variable, for instance to uncapitalized c ? Currently, there's even more confusion when Check'ing Cconj_opp :
Actually, Coq noticed the name clash ... and displays instead C0, i.e the zero of complex numbers ! (I guess it has something to
do with C0 being a notation).
The text was updated successfully, but these errors were encountered:
Just a minor remark :
QuantumLib.Complex.Cconj_opp
uses a variable named capitalizedC
, which is unfortunate, sinceC
is here the type of the complex numbers. Even if that doesn't prevent from using this lemma, could you rename this variable, for instance to uncapitalizedc
? Currently, there's even more confusion when Check'ingCconj_opp
:Actually, Coq noticed the name clash ... and displays instead
C0
, i.e the zero of complex numbers ! (I guess it has something todo with
C0
being a notation).The text was updated successfully, but these errors were encountered: