command expected_choose

Stream: new members

[Marianne]

Here I want lean to commute "8! / (8-4)! ". The Lean Infoview reports that command expected at line 5, and it doesn't work out the result as well at line 7, but I don't really know how I should correct it. Is the definition not enough?

[Marianne]

image.png

[Kevin Buzzard]

Is this lean 3? Why don't you upgrade?

[Damiano Testa]

Also, you probably need to add open_locale nat.

[Marianne]

Kevin Buzzard said:

Is this lean 3? Why don't you upgrade?

Yeah this is lean 3...I work together with a group and they told me to maintain Lean 3.51.1

[Marianne]

Damiano Testa said:

Also, you probably need to add open_locale nat.

Oh, this really help! May I ask what's the difference here?

[Damiano Testa]

It instructs lean to use special notation, open namespaces, possibly add instances...

[Damiano Testa]

In this specific case, the notation ! is not globally available, but it is inside the locale nat.

[Marianne]

I see...open_locale nat seems to denote what "!" functions in the local context.

[Marianne]

Thank you!