avoid use of tauto?

Stream: general

[Kayla Thomas]

I think I read somewhere to avoid the use of finish? Does the same hold for tauto? Is it best to avoid it if possible because it may slow down the type checking of the program?

[Kevin Buzzard]

Right now mathlib avoids using finish because it's (a) slow and (b) possibly not going to be ported to lean 4. But you can use what you like! It all depends on what you're doing. One practical reason to avoid finish is that if you use it in the middle of a lean 3 proof then you might find that later stages of the proof become tedious to write because Lean keeps running finish so you have to wait 5 seconds before you can see the output of what you just typed. tauto can be much quicker though. It's easy to check that there are many many occurrences of tauto in mathlib3, so it's acceptable there -- but, again, if you're just doing an independent project then you can do what you want!

[Kayla Thomas]

Ok. Thank you!