invalid end

Stream: lean4

[Dean Young]

What does this error entail?

invalid 'end', insufficient scopes

suppose I want to finish some code later in between a begin ... end... what is a placeholder?

[Notification Bot]

A message was moved here from #lean4 > Failed to show termination on mutual theorems by Reid Barton.

[Reid Barton]

It sounds like the kind of error you would get by having more ends than commands that should be paired with end (e.g. section, namespace)...?

[Mario Carneiro]

If you are using begin ... end in lean 4 that might explain it, this is not legal syntax anymore

[Mario Carneiro]

it is by ... now