From c6f04a9f5659f594a098d28697cb525f34f6cdad Mon Sep 17 00:00:00 2001 From: Isaac Date: Tue, 19 Apr 2022 13:19:17 -0700 Subject: [PATCH] error messages --- __pycache__/proof.cpython-39.pyc | Bin 22742 -> 22948 bytes abelian_proof.py | 4 +- proof.py | 262 ++++++++++++++++--------------- 3 files changed, 135 insertions(+), 131 deletions(-) diff --git a/__pycache__/proof.cpython-39.pyc b/__pycache__/proof.cpython-39.pyc index 325fdf2242c75580b9b8bb5dce2fa89529fcb8e5..13f7c975075310a6cd3ca271158f0a2e85ed4203 100644 GIT binary patch delta 5029 zcmb_g4Qw3672ess+gtD5*^YnC|L2Qyc6{+qd^oWklOGe?iIX_CA+`ahA(-qD&T-E6 zcunB6#t8+Uudvu;<4*UJOgn!G6_Fi}B&{LT~FMAB0j~2j&%nWuM zdc0RhA2BttECl-Kz`WycD zkHT5+OYqIC-Oaoa-R+5FaPpg%lUYM%EtzIAO=P@ea>?Y7X@TMLTzJLrh4tA%^l5i? zL*b9G!;(fMixo-Jipeb5lxJoB7k4i{5 zbKbOU8FTX}eiHg}s^lph4&|K5Ux)WY+Gsox>zO(@$uA{W)hQw31X@K)egtRB8w5Rvm__;o?k=X9g-OSl2g6us!%hSTmB z*zoOedvSE_4#J@uO(ci!r0X6s7c8h)#t3!vk_p0Jiwj--cnQ&hJed!O6>TWVTbv3n zxkBarmNMstcS=fXRD+#|n~J!31a3Jk?PqXjSOAmy?-jBsCkIO1t$yd6Yc|rz=V^L|?5a15fCR z=AW2;L$+9fWMH(LUP~Eq&*GgE_x?|-ffEBqLmHd$>-{&xLb1` zW+&yq= z3zy>PFNRmlxUs7p&&ebj6Sc-@CY($<$j7OAdWxq7-GF_HD%Q~bznbU5|HRraJ zlc+5d6_(_ZMpV=v*DQ0wA8CwjnvuHKkk%Q3)&Wx|TH}fdwIUI*CCUX8m8YS%s?uRj zMO9sS#3#ga!96~9D8>=io5sfyxMaMKCesTKRh7c?+uS7!F7xK`SVZMSo&|S2F+OE3 zDEKt*gV(F-%0dh$mxq0lTW2aBF6P4{4|$KQFIibW?F)=C4BAnAUB&wyJ2a(5c)BP%x zOb=qDIT$I1YIsc4GE(%E&>9*>SO&bg@@bvpgrxp0$%qa=uO4&|J6>HIi|BT`smA^x zLBsC&q-p1u5p3f@GD5``LvR$^A|4w&*TJb#laFD`0*ei0PR0}aM`Pw#qWy;0z5_f& zZ(lD+G!yYxMhVwaY_oCI5LXQk6;EBxM05qdKa5l^Qfv+%PGft=Qi`D_x(s%bA<>Xt zv&@hY%_dVd6oKZ0NI`5zs3(^CF&5}oSJiW6D1|88svOEqwutLRqpDksmWIj|fzfiJLEMic} zMDeGYnKq6mTn>uzF6mT8@<~19{B1K(+hNPv$JbLemMqpqL)^SMv~M`E(hOY}3k{EB zu*HmIew?1AuGnb&U_2obvz@rX*R;AUlJyy-8jLlSH7qXH`9gTg;S{9{E=na4vPpQh zsZj+2vkG2sDf8*FCI}-WuA;f(i-1W`5}^NQF!?R$^LaBbv#V*E%91LTZfDTIk*56Y z^JmWw3*tQ2;#Hr%_*~~dZW(4uK<|gWt%a&6fSX~uwVWB^&C{(}?A-j%S~oByh|m1{ z(#kAS!v*ECgs~v^a=sZF*VnQ^df4yfF=J|9tb1&KeBXQXhu7CI)(%f>D9-*Wxp)T| z5%ssjxee{?Z}Y_)Utp?T@51jlg;nA%_lt2uZJF$2SlxCNyAO`GC86t5zk+FCKIgLS zjBSQJn+uE6JFSSzj?DBDLv$b?9^JgGBtypaCAE<}6red6p5c@%oZWm$$iNZuGfuv4>9{wulm_%U0~W$> zJ8Bns^fKghHsEyHJ1aMinjQm1h)MWgv2e3%d1hT$W7Oj2P`0!pX+*KySc}}VlLEpI0QX#@aaCqxF zdk1kGp5NNIyoM$qN&pY0dpTPa0C{LB`J+`Jx2uKS1KnLin_5!PO(w}r0iC_UN$uDJ zqFq5q&ug~$FNOQ&7aPuje>6MnF*9DgEsb=z{* z0UvA&utHF`uVM=j-5y}SfUfP(e9rVzQ6MDBLoTJ{34cDI9}&Tfs!J2R z)ECC-{H3pf-2%bOyBQ~p;mGCmJ*?r7v33e|mfB9C@XqCL%ls1f@f8uB!hOg^at>$v z3IcZ8q_&LMjimPbVo|&F%<$k|trMTSbAHXP7bv~CeAVp>}U^4Np0d!S8s=e8|n4H-_-`Gf|i_Dc|t|IdlGJDAECvyXtaWa!+ZX|Pvj74Ue z%n>rTl9?rQl+4%293%5}GIx;yGPHl;4@iY*AEe6@WF96nN9Gau*OeU|+1fHK507P9 vKr6r_3y|{w){fI_`%y?AjZZr!C=54HO3M~MwZ2TA;ejS zv~H3H$dGcTc|b{VhLVsb84`Cw+ho#5el*ib(oEB7CZ06Y_D83$Y3OrOW}4|acV#K2 zNeI)acl^!n-TOHAyXSo8tS-#5Up&w3LpeEC0soHX5AJ*W@bh+`4IWwIwQ5W^Y2vh~ z9*3}Pckqm+L?m52D@4raOw)`B2?uXsnU;v$Cj>3AKxw#AuIV+h4k2$~V zZo|0;lz1!=4IdtxP*>3UD`6zBljXzZylQq4-p%u|)3YDuHL<*X+M)=~e^xjr@)@N* z0ovW3C5q8D!deAU7REDn5%#prKz)@F4V zPQD46OB*1kwA`989L7qE+?=?DcB%v1`!AO|Jio=E6J)d?JJ`ppdZ)CJy$D(UV)g{& zmX|<>f7_B5v>c+;BScIdK{t(>JwhtZa~4K^DhyutE37hm`+=xG8s{|luetrP34dZ- z^T!f?4PT6?TR|?v-+x72QsAe}P~v!5~6d-AlLoIA>QYtaxznOj!}G=na$)OZct>|0i?= z4fR7~(<1l43QdfN8u}V(MJk$2eb{4EnnD^!%~PfkVM@|u9V2~%aJzlVtV`!Dx@iWL zccX|>ZZepimL?TVqMciZIl%z|#>7Yq%L3X%iq8B48hgvintj6N0_XJzgG8$gH|IUWE5l+ zUk-3r+7g@4)EGV*Qp43K9m(@-Nn?lOnwr2~b1Vuc>k32J!{cN7P|CLw>r05bLVTN{ zPGR#GMibFjUK1EhQ+ENo-UM~rNl3UN(hNgavFOq?i0extr7jXju3ft5u8eX0jaKtPQXU_rDOkidAl&lug+5fF{4pCH0x>0(`8a6K_d zZ5ak-W<}Ri&;=z#y60~AeqC*b$1^zK|G?wc`l4KeKV{za1{GMl$*XWTQzjpSf7P_X z-r7RA8qR@xYn>2isLAEzsV20^pf3owHPj+~_ct``4cb1NK2@V(JlkF8f}g=;gvR&@ z4q+a2wel0-9@&Hby8FhQ%7$-_EV*2PF=tdWq7i+(t}&_^a~~FS7+&)1%1{<#YoM#K zvzeDvq{xOgXNs#5YD-sG^SO|UA9XqWxUsq*Np?B#S&*%Gu3qM270fF77|2VXtNc86 zOwPgTPz8Ln^jGp4n)eR)eN%&tn_yUkNugL&kCJ-@Z1L!RtuGddPHa4M&!;YZWLX9L zG%w35V~=zJD5eX*SK$5D>5dCj$?|9u`vj8YX*MNmqK0L#Jb=)1mlt znViheWD_ZwERwEKL^?$;lSHm$-Em*xtWhKfrA$F&7OdUu6&&MYNZGEbSdmXh;}XZwi9Vw zV=XSsoIW&y3RV|9-c`eX1~2zi!PTzm`ZqP(yi}1LhD_lHJC+Dsz?9UtB#Kio3!du! zGo0PBzOsvU*^O{1`+5n=L|`+RdK%;;b=?82J#B0oBzubSQ}@B12Jf5LoK{)-%r<^O z_#V97b85*?aCwO@Z@$hbOi@UTC1n(&Bb$5`p6>R+mGG1D!?aciV!a{vBXpZKQ+<>k zAEN-b4G$%Tqwy`6686Izy=2cHdh1yNyj%Bp=!Xh^5)sqKzM;)O%-`ZhoqG|XJ zn<1yi1F!TcvZ0~y)U6>l3Gd#z1*fXqMpMbg=jHs514aUcbK8Ci$NDPSy>PM5?=q4i z&N`44Jwnnm9BqWJ*16$>K7~Cn`(fX!jID#0cdTF=c)VHrUF=aP?QgeAIEY8UaftP= zXZOJ~{k7%y;i5dz;0em}=bGAyg~(FR!AJdtawiU+EQQjY70|h}icLduXOJt+vpW^` zO?YwV)zt*I5cCu5B)E-W55azd5rT07mEbVJ5rVr2=vzp=hv16@Un01l;41_V z5F95sMR1znYXoNmFXCCc{W`(p1m7T-f#hxvyuYhHut;$zF1&J;JjH{T1Ftf?>`IPe U!+)o;Nby2ww~zHg@9rJ{0mugv>i_@% diff --git a/abelian_proof.py b/abelian_proof.py index 38b8615..043d56a 100644 --- a/abelian_proof.py +++ b/abelian_proof.py @@ -14,7 +14,7 @@ p.closure(G,'a','b') p.accessAssumption() p.forallElim(4,['a * b']) -p.leftMult('a',5) # G.elements should be a function not a dictionary +p.leftMult('a',5) p.forallElim(4,['a']) p.substituteRHS(6,7) p.identleft(8) @@ -24,4 +24,4 @@ p.substituteRHS(11,12) p.identleft(13) p.forAllIntroduction(14,["a","b"],[1,2]) -p.qed(15) +p.qed(15) \ No newline at end of file diff --git a/proof.py b/proof.py index 42dfb3f..a5a41d4 100644 --- a/proof.py +++ b/proof.py @@ -102,9 +102,9 @@ def substituteRHS(self, lineNum1, lineNum2): self.justifications += [f'Replaced all instances of {ev2.LHS} with {ev2.RHS} on line {lineNum1}'] self.show() else: - print(f"The statement on line {lineNum2} is not an equality, substitutition is not possible") + print('\n'+f"The statement on line {lineNum2} is not an equality, substitutition is not possible") else: - print(f"The statement on line {lineNum1} is not an equality, substitutition is not possible") + print('\n'+f"The statement on line {lineNum1} is not an equality, substitutition is not possible") def substituteLHS(self, lineNum1, lineNum2): """ @@ -121,9 +121,9 @@ def substituteLHS(self, lineNum1, lineNum2): self.justifications += [f'Replaced all instances of {ev2.RHS} with {ev2.LHS} on line {lineNum1}'] self.show() else: - print(f"The statement on line {lineNum2} is not an equality, substitutition is not possible") + print('\n'+f"The statement on line {lineNum2} is not an equality, substitutition is not possible") else: - print(f"The statement on line {lineNum1} is not an equality, substitutition is not possible") + print('\n'+f"The statement on line {lineNum1} is not an equality, substitutition is not possible") def modus(self, lineNum1, lineNums): # lineNums because multiple assumptions may be neccessary (I think) """ @@ -143,9 +143,9 @@ def modus(self, lineNum1, lineNums): # lineNums because multiple assumptions may self.justifications += [f'Modus Ponens on {str(lineNum1)}, {str(lineNums)}'] self.show() else: - print (f"Line {str(lineNum1)} is not an implies statement") + print ('\n'+f"Line {str(lineNum1)} is not an implies statement") else: - print("The second argument should be a list, maybe you only have one assumption - make sure to put it into a singleton list") + print('\n'+"The second argument should be a list, maybe you only have one assumption - make sure to put it into a singleton list") def inverseElimRHS(self,lineNum): """ @@ -170,13 +170,13 @@ def inverseElimRHS(self,lineNum): lawApplied=True break if lawApplied==False: - print (f"Inverse laws can't be applied on line {lineNum}") - return - self.steps += [newProducts] - self.justifications += [f'Right hand side inverse elimination on line {lineNum}'] - self.show() + print ('\n'+f"Inverse laws can't be applied on line {lineNum}") + else: + self.steps += [newProducts] + self.justifications += [f'Right hand side inverse elimination on line {lineNum}'] + self.show() else: - print(f"It doesn't seem like line {lineNum} contains an equation") + print('\n'+f"It doesn't seem like line {lineNum} contains an equation") def inverseElimLHS(self,lineNum): @@ -202,13 +202,13 @@ def inverseElimLHS(self,lineNum): lawApplied=True break if lawApplied==False: - print (f"Inverse laws can't be applied on line {lineNum}") - return - self.steps += [newProducts] - self.justifications += [f'Left hand side inverse elimination on line {lineNum}'] - self.show() + print ('\n'+f"Inverse laws can't be applied on line {lineNum}") + else: + self.steps += [newProducts] + self.justifications += [f'Left hand side inverse elimination on line {lineNum}'] + self.show() else: - print(f"It doesn't seem like line {lineNum} contains an equation") + print('\n'+f"It doesn't seem like line {lineNum} contains an equation") ## For all and there exists elimination @@ -219,13 +219,14 @@ def forallElim(self, lineNum, replacements): :param replacements: the list of elements to replace the existential elements """ evidence = copy.deepcopy(self.steps[lineNum]) - if isinstance(evidence, forall) == False: - print(f"There is no forall statmenent on line {lineNum}") - else: + if isinstance(evidence, forall): expr = evidence.replace(replacements) self.steps += [expr] self.justifications += [f'For all elimination on line {lineNum}'] self.show() + else: + print('\n'+f"There is no forall statmenent on line {lineNum}") + def thereexistsElim(self, lineNum, replacements): # We can only do this once! """ @@ -234,13 +235,14 @@ def thereexistsElim(self, lineNum, replacements): # We can only do this once! :param replacements: the list of elements to replace the existential elements """ evidence = copy.deepcopy(self.steps[lineNum]) - if isinstance(evidence, thereexists) == False: - print(f"There is no there exists statmenent on line {lineNum}") - else: + if isinstance(evidence, thereexists): expr = evidence.replace(replacements) self.steps += [expr] self.justifications += [f'There exists elimination on line {lineNum}'] self.show() + else: + print('\n' + f"There is no there exists statmenent on line {lineNum}") + ## Multiplication manipulation def leftMult(self, elemName, lineNum): @@ -259,9 +261,9 @@ def leftMult(self, elemName, lineNum): self.justifications += ['Left multiply line {lineNum} by ' +str(elem) ] self.show() else: - print("The element " + elemName + " is not in the group " + eq.group) + print('\n' + "The element " + elemName + " is not in the " + str(eq.group)) else: - print (f"Line {lineNum} is not an equation") + print ('\n' + f"Line {lineNum} is not an equation") def rightMult (self, elemName, lineNum): """ @@ -279,67 +281,70 @@ def rightMult (self, elemName, lineNum): self.justifications += ['Right multiply line {lineNum} by ' +str(elem) ] self.show() else: - print("The element " + elemName + " is not in the group " + eq.group) + print('\n' + "The element " + elemName + " is not in the " + str(eq.group)) else: - print (f"Line {lineNum} is not an equation") + print ('\n' + f"Line {lineNum} is not an equation") ##power methods def breakPower(self,input): """ Given an expression like e^a where a is a python integer, return a mult object equivalent to e^a :param power: the power to be converted to mult """ - if isinstance(input,power) == False: - print (f"Expected a power object but received type {type(input)}") - return - exp=input.exponent - element = input.element - multList=[] - for i in range(exp): - multList.append(element) - self.steps += [Mult(multList)] - self.justifications += ['Convert power object to mult object'] - self.show() + if isinstance(input,power): + exp=input.exponent + element = input.element + multList=[] + for i in range(exp): + multList.append(element) + self.steps += [Mult(multList)] + self.justifications += ['Convert power object to mult object'] + self.show() + else: + print ('\n'+f"Expected a power object but received type {type(input)}") def combinePower(self, mult): """ Given a mult object with a single element, convert it to a power object (for example turning e*e*e to e^3) :param mult: the mult object to be converted """ - if isinstance(mult,Mult) == False: - print (f"Expected a Mult object but received type {type(mult)}") - return - multList=mult.elemList - e=multList[0] - for i in multList: - if i != e: - print ("Need a single element but given multiple") - return - result=power(e,len(multList)) - self.steps += [result] - self.justifications += ['Convert multiplications to equivalent powers'] - self.show() + if isinstance(mult,Mult): + multList=mult.elemList + e=multList[0] + singletonCheck = True + for i in multList: + if i != e: + singletonCheck = False + if singletonCheck == False: + print ('\n' +"Need a single element but given multiple") + else: + result=power(e,len(multList)) + self.steps += [result] + self.justifications += ['Convert multiplications to equivalent powers'] + self.show() + else: + print ('\n' +f"Expected a Mult object but received type {type(mult)}") def splitPowerAddition(self,input): """ Simplify power objects: Given an expression e^a+b, convert to e^a*e^b. Given an expression e^a*b=(e^a)^b :param power: the power object with addition in exponent to be modified """ - if isinstance(input, power) == False: - print (f"Expected a power object but received type {type(input)}") - return - element = input.element - exp=input.exponent - l=exp.split("+") - if len(l)==1: - print ("No power addition to be split apart") - return - multList=[] - for i in l: - elem=power(element,i) - multList.append(elem) - self.steps += [Mult(multList)] - self.justifications += ["split up power with addition in exponents"] - self.show() + if isinstance(input, power): + element = input.element + exp=input.exponent + l=exp.split("+") + if len(l)==1: + print ('\n'+"No power addition to be split apart") + else: + multList=[] + for i in l: + elem=power(element,i) + multList.append(elem) + self.steps += [Mult(multList)] + self.justifications += ["Split up power with addition in exponents"] + self.show() + else: + print ('\n'+f"Expected a power object but received type {type(input)}") def splitPowerMult(self,input): @@ -347,22 +352,22 @@ def splitPowerMult(self,input): Simplify power objects: Given an expression e^a*b=(e^a)^b :param lineNum: the power object with mult in exponent to be modified """ - if isinstance(input, power) == False: - print (f"Expected a power object but received type {type(input)}") - return - element = input.element - exp=input.exponent - l=exp.split("*") - if len(l)==1: - print ("No power multiplication to be split apart") - return - elem=element - for i in l: - e=power(elem,i) - elem=e - self.steps += [elem] - self.justifications += ["split up power with multiplication in exponents"] - self.show() + if isinstance(input, power) == False: + element = input.element + exp=input.exponent + l=exp.split("*") + if len(l)==1: + print ('\n'+"No power multiplication to be split apart") + else: + elem=element + for i in l: + e=power(elem,i) + elem=e + self.steps += [elem] + self.justifications += ["Split up power with multiplication in exponents"] + self.show() + else: + print ('\n'+f"Expected a power object but received type {type(input)}") ## Identity and equality elimination def rightSidesEq(self, lineNum1, lineNum2): @@ -378,8 +383,7 @@ def rightSidesEq(self, lineNum1, lineNum2): self.justifications += [f"Equations with same right side on lines {str(lineNum1)}, {str(lineNum2)}"] self.show() else: - print (f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same right sides") - return + print ('\n' +f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same right sides") def leftSidesEq(self, lineNum1, lineNum2): """ @@ -394,8 +398,7 @@ def leftSidesEq(self, lineNum1, lineNum2): self.justifications += [f"Equations with same left side on lines {str(lineNum1)}, {str(lineNum2)}"] self.show() else: - print (f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same left sides") - return + print ('\n' +f"The equations on lines {str(lineNum1)}, {str(lineNum2)} do not have the same left sides") def identleft(self, lineNum): """ @@ -419,18 +422,17 @@ def identleft(self, lineNum): break # else we can't apply identity elimination if l1==[]: - print ("identity can't be applied") - return - newProduct = Mult(l1) - ret = Eq(newProduct,evidence.RHS,evidence.group) + print('\n' +"Identity can't be applied") + else: + newProduct = Mult(l1) + ret = Eq(newProduct,evidence.RHS,evidence.group) + self.steps += [ret] + self.justifications += ["identity elimination "] + self.show() else: - print(f"Expected an equation on line {lineNum} but received {type(evidence)}") - return - - self.steps += [ret] - self.justifications += ["identity elimination "] - self.show() + print('\n' +f"Expected an equation on line {lineNum} but received {type(evidence)}") + def identright(self, lineNum): """ Identity elimination: find the first pair of element and the group identity return an element @@ -453,17 +455,17 @@ def identright(self, lineNum): break # else we can't apply identity elimination if l1==[]: - print ("identity can't be applied") - return - newProduct = Mult(l1) - ret = Eq(evidence.LHS,newProduct,evidence.group) + print ('\n' + "Identity can't be applied") + else: + newProduct = Mult(l1) + ret = Eq(evidence.LHS,newProduct,evidence.group) + self.steps += [ret] + self.justifications += ["identity elimination "] + self.show() else: - print(f"Expected an equation on line {lineNum} but received {type(evidence)}") - return + print('\n' + f"Expected an equation on line {lineNum} but received {type(evidence)}") - self.steps += [ret] - self.justifications += ["identity elimination "] - self.show() + def introReflexive(self,eq): """ @@ -477,7 +479,7 @@ def introReflexive(self,eq): self.justifications += ["reflexive equality"] self.show() else: - print ("this is not reflexive") + print ('\n' + "This is not reflexive") def reduceLogic(self, lineNum): """ @@ -490,7 +492,7 @@ def reduceLogic(self, lineNum): self.justifications += ["logic reduction"] self.show() else: - print ("this is not a logic statement") + print ('\n' + "This is not a logic statement") def introCases(self, case): """ @@ -500,7 +502,7 @@ def introCases(self, case): case1 = case case2 = reduce(Not(case)) self.steps += [Or(case1, case2)] - self.justifications += ["case introduction (LEM)"] + self.justifications += ["Case introduction (LEM)"] self.show() def introSubproof(self, assum): @@ -530,9 +532,10 @@ def concludeSubproof(self, lineNum): self.justifications += [None]*((len(evidence.steps))-evidence.linestart-1) self.steps += [conc] self.justifications += ["Conclusion of subproof"] + self.show() else: print("You can only conclude a subproof right after one") - self.show() + def introElement(self,G, name): """ @@ -542,7 +545,7 @@ def introElement(self,G, name): :param name: the name of the new element """ if G.contains(name): - print(f"{name} is already in {G}") + print('\n' + f"{name} is already in {G}") else: self.env[name] = G.newElement(name) self.steps += [In(name, G)] @@ -563,15 +566,16 @@ def forAllIntroduction(self, equationLine, vars, elemIntroLines): v = vars[i] l = elemIntroLines[i] if self.steps[l].elem!=vars[i]: + print('\n') print("Line", l, "does not introduce variable", v) - return - if self.steps[l].group!=G: + elif self.steps[l].group!=G: + print('\n') print("Element", v, "is not in group", G) - return - #If you make it here, this is a valid for all intro - self.steps+=[forall(vars,G,evidence)] - self.justifications+=["For all introduction"] - self.show() + else: + #If you make it here, this is a valid for all intro + self.steps+=[forall(vars,G,evidence)] + self.justifications+=["For all introduction"] + self.show() def closure(self,G,a,b): ''' @@ -587,9 +591,9 @@ def closure(self,G,a,b): self.show() else: if not G.contains(a): - print(f"{a} is not in {G}") + print('\n'+f"{a} is not in {G}") else: - print(f"{b} is not in {G}") + print('\n'+f"{b} is not in {G}") def cancelRight(self, lineNum, mult): ''' @@ -607,9 +611,9 @@ def cancelRight(self, lineNum, mult): self.justifications += [f"Right side cancellation of {mult} on line {lineNum}"] self.show() else: - print(f"It seems like the right hand sides on line {lineNum} are not equal to {mult}") + print('\n'+f"It seems like the right hand sides on line {lineNum} are not equal to {mult}") else: - print(f"It doesn't seem like line {lineNum} contains an equation") + print('\n'+f"It doesn't seem like line {lineNum} contains an equation") def cancelLeft(self, lineNum, mult): ''' @@ -627,9 +631,9 @@ def cancelLeft(self, lineNum, mult): self.justifications += [f"Right side cancellation of {mult} on line {lineNum}"] self.show() else: - print(f"It seems like the left hand sides on line {lineNum} are not equal to {mult}") + print('\n'+f"It seems like the left hand sides on line {lineNum} are not equal to {mult}") else: - print(f"It doesn't seem like line {lineNum} contains an equation") + print('\n'+f"It doesn't seem like line {lineNum} contains an equation") def switchSidesOfEqual(self, lineNum): ''' @@ -644,7 +648,7 @@ def switchSidesOfEqual(self, lineNum): self.justifications += [f"Switched sides of line {lineNum}"] self.show() else: - print(f"Hmm, it doesn't look like line {lineNum} isn't an equality") + print('\n'+f"Hmm, it doesn't look like line {lineNum} isn't an equality") def notElim(self, lineNum1, lineNum2): ''' @@ -659,7 +663,7 @@ def notElim(self, lineNum1, lineNum2): self.justifications += [f'Contradiction from lines {lineNum1} and {lineNum2}'] self.show() else: - print(f"The statement on line {lineNum1} isn't a Not statement") + print('\n'+f"The statement on line {lineNum1} isn't a Not statement") def impliesIntroduction(self, lineNumsAssums, lineNumConc): # needs work, a lot of it ''' @@ -689,7 +693,7 @@ def andElim(self, lineNum, n): self.steps += [evidence.arg2] self.justifications += ["And elimination"] else: - print("You must choose argument 1 or 2") + print('\n'+"You must choose argument 1 or 2") else: - print(f"The statement on line {lineNum} isn't an And statement") + print('\n'+f"The statement on line {lineNum} isn't an And statement") \ No newline at end of file