right thinks it's left

Stream: general

[Yaël Dillies]

Someone somewhere is guilty of overzealous copy-pasting :stuck_out_tongue:

example : true := by right
/-
left tactic failed, target is not an inductive datatype with two constructors
state:
true
-/

[Damiano Testa]

Maybe it is assuming that after right you will try left and is saving you the trouble...

[Mauricio Collares]

This can easily be fixed by printing the error message upside down

[Julian Berman]

I don't think you entered tactic mode the right way:

Screenshot-2023-05-23-at-09.41.24.png