Error in Math in Lean example

Stream: new members

[eviedot]

Hi all, I'm new to Lean and working my way through Mathematics in Lean. For this example in section 2.1:

example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by
  sorry

I get the error:

typeclass instance problem is stuck, it is often due to metavariables
  HAdd ?m.195 ?m.196 ?m.206

Is there a solution or should I just move on?

[Patrick Massot]

You need to be more specific: how do you hit this error?

[Patrick Massot]

Did you follow the instructions to get the book on your computer and open the exercise file? Are you trying to use it on GitPod?

[eviedot]

Apologies. I have Lean installed and using vscode in Windows 11. All the example code in MIL so far works fine, and I've been able to prove the requested exercises, but the above code, when pasted into vscode, immediately gives the above error, and when I try to write tactics they are ignored.

[Patrick Massot]

You are not meant to paste this in an empty file.

[Patrick Massot]

You need to follow instructions at https://github.com/leanprover-community/mathematics_in_lean#to-use-this-repository-on-your-computer

[Patrick Massot]

And then this exercise will live a happy life inside https://github.com/leanprover-community/mathematics_in_lean/blob/master/MIL/C02_Basics/S01_Calculating.lean

[eviedot]

Ah I see. I've been simply appending to S02_Overview.lean. When I paste it into S01_Calculating.lean I get the same error with different numbers:

typeclass instance problem is stuck, it is often due to metavariables
  HAdd ?m.14639 ?m.14640 ?m.14650

I followed the instructions to set up lean and clone MIL last night, if that helps.

[Patrick Massot]

You don't have to paste it, it's already there.

[eviedot]

Oop I see. Thanks. Is there anything I need to do to remove the error from the second copy, or I should just ignore it?

[eviedot]

Oh looking at the surrounding code I see that the error is from missing variable statement. Thank you for your help.

[Patrick Massot]

Indeed the error says Lean had no idea what kind of mathematical objects you were manipulating, hence it couldn't make sense of the + sign. You will understand the details of this error message much later.