Zulip Chat Archive

Stream: new members

Topic: Error import tactic

Gemma Crowe (Jun 22 2021 at 10:47):

Hello! I'm very new to Lean and going through the YouTube videos from the workshop last year. Could I get some help? Please send to a different chat topic if I'm asking in the wrong place.

I've been going through the proof from https://www.youtube.com/watch?v=b59fpAJ8Mfs and my code comes up with an error when I add
import tactic.linarith

It's saying this is an invalid import command, any ideas why? Everything else works in the proof up to then.


Anne Baanen (Jun 22 2021 at 10:48):

Could you post a copy of your code (see also #backticks for tips on how to format it) and the complete error message?

Anne Baanen (Jun 22 2021 at 10:49):

And welcome to the Zulip chat, you're definitely asking in the right place here.

Eric Rodriguez (Jun 22 2021 at 10:49):

sometimes Lean gets confused, can you try the restart Lean command one time first?

Gemma Crowe (Jun 22 2021 at 10:52):

@Eric Rodriguez that worked! I just restarted it and it's all fine now, thanks! Does this happen a lot with Lean, that it gets confused?

Eric Rodriguez (Jun 22 2021 at 10:53):

yeah, I find that sometimes working with new files it does that, not sure why...

Last updated: Dec 20 2023 at 11:08 UTC