Zulip Chat Archive

Stream: new members

Topic: Lean 4 cannot eval issue

Atieh Hosseinizadeh (Feb 21 2023 at 19:08):

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 (Feb 21 2023 at 19:09):

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 (Feb 21 2023 at 19:10):

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

Atieh Hosseinizadeh (Feb 21 2023 at 19:11):

Thank you
Sorry I didn't know

Alex J. Best (Feb 21 2023 at 19:12):

No problem! just helps us keep things organised

Last updated: Dec 20 2023 at 11:08 UTC