unknown identifier 'begin'； unexpected token ','

Stream: new members

[Oliver]

Why does it say
“mathlib-demo.lean:48:0

unknown identifier 'begin'

All Messages (3)

mathlib-demo.lean:48:0

unknown identifier 'begin'

mathlib-demo.lean:49:10

unexpected token ','; expected command

mathlib-demo.lean:60:0

invalid 'end', insufficient scopes

Error: Connection to server got closed. Server will not be restarted.

Source: Extension

Go to output

Connection to server got closed. Server will not be restarted.
*”
For:

begin

  intros h,

  cases h with x hx,

  use x,

  split,

  { exact hx.1 },

  split,

  { exact hx.2 },

  { intros x' hx',

    -- Here, you would provide a valid proof showing l1_norm x ≤ l1_norm x'

    sorry -- Placeholder for the detailed proof

  }

end

Thanks。

[Kyle Miller]

(Zulip hint: #backticks)

It looks like you're using Lean 4 to try to run Lean 3 code

[Oliver]

Kyle Miller said:

(Zulip hint: #backticks)

It looks like you're using Lean 4 to try to run Lean 3 code

Then how to modify or revise the code to be run on Lean 4? Thanks

[Kyle Miller]

Lean 4 is a very different language, so it would need to be rewritten.

Where did you get this mathlib-demo.lean? Could you share a url?

[Oliver]

Is there is s

Kyle Miller said:

Lean 4 is a very different language, so it would need to be rewritten.

Where did you get this mathlib-demo.lean? Could you share a url?

How to modify or revise the code to be run on Lean 4? Shouldn't there be a simple modification on this simple code? Thanks

[Oliver]

Does anyone know how to modify or revise the code to be run on Lean 4? Thanks a lot.

[Kim Morrison]

Please, use #backticks as you've been asked above, and explain where this code came from.

[Kim Morrison]

Translating from Lean 3 to Lean 4 is not "simple" (although there are automated tools which work well, although you need to be an expert to use them :-)

[Oliver]

used [#backticks]; How to convert it into Lean 4 code? Thanks.

[Kim Morrison]

Please read #mwe. Also, I would suggest that you are not putting sufficient effort into asking your questions. You haven't answered Kyle's question above, despite me repeating it.

[Notification Bot]

This topic was moved here from #lean4 > unknown identifier 'begin'； unexpected token ',' by Kim Morrison.

[Jon Eugster]

Based on that comment line and the type of question, I am assuming they got the code from a LLM and copy-pasted it into the Lean4 web editor:sweat_smile: mathlib-demo.lean is simply what the web editor displays in the infoview and probably does not corrspond the a file existing on the web.

Most important changes are

• begin ... end is now by+indent
• no commas, no {}
• cases to cases'

However, as people mentioned, if you provide a better example including the imports and theorem statement, it's easier to help you. Just seeing a proof like this means nobody can actually try to get the code running, as the essential information is missing, so it's less likely people take the time to answer :)

[Ralf Stephan]

Yeah, and LLMs even give Lean3 code if you ask them for Lean4. They just have learned Lean3, missing newer web pages.

[Damiano Testa]

Maybe there should be a linter that flags uses of := begin saying "Lean 3 is out of fashion, give := by a try".