Lean 4 cannot eval issue

Stream: new members

[Atieh Hosseinizadeh]

Hello everyone, I've started to work with Lean4 recently and when I want to evaluate a simple code, it doesn't work. I run the below code:
def n : nat := 2
#eval n +2

but I got this error:
cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
Anybody knows what I should do?

[Alex J. Best]

You should ask your question in a new thread next time.
But i think the issue is that in Lean 4, nat is now Nat with a capital n, so Lean doesn't know what it is in what you've got

[Notification Bot]

2 messages were moved here from #new members > Naming inconsistencies by Alex J. Best.

[Atieh Hosseinizadeh]

Thank you
Sorry I didn't know

[Alex J. Best]

No problem! just helps us keep things organised