Lean에게 표현식을 평가하도록 요청하려면 편집기에서 표현식 앞에 #eval을 작성하십시오. 그러면 편집기가 결과를 보고합니다. 일반적으로 결과는 커서나 마우스 포인터를 #eval 위에 올려 확인할 수 있습니다. 예를 들어,

3#eval 1 + 2

다음 값을 산출합니다.

3

Lean은 산술 연산자에 대해 일반적인 우선순위 및 결합성 규칙을 따릅니다. 즉,

11#eval 1 + 2 * 5

15가 아니라 11이라는 값을 산출합니다.

일반적인 수학 표기법과 대부분의 프로그래밍 언어는 함수를 인자에 적용할 때 괄호를 사용하지만(예: f(x)), Lean에서는 함수를 인자 옆에 나란히 쓰기만 하면 됩니다(예: f x). 함수 적용은 가장 흔히 쓰이는 연산 중 하나이므로 간결하게 표기하는 편이 유리합니다. 다음과 같이 쓰는 대신

#eval String.append("Hello, ", "Lean!")

"Hello, Lean!"을 계산하려면 대신 다음과 같이 작성합니다

"Hello, Lean!"#eval String.append "Hello, " "Lean!"

여기서 함수의 두 인자는 공백으로 구분하여 함수 바로 옆에 적기만 하면 됩니다.

산술의 연산 순서 규칙 때문에 표현식 (1 + 2) * 5에 괄호가 필요한 것처럼, 함수의 인자를 다른 함수 호출로 계산해야 할 때에도 괄호가 필요합니다. 예를 들어, 다음 식에서는 괄호가 필요합니다.

"great oak tree"#eval String.append "great " (String.append "oak " "tree")

그렇지 않으면 두 번째 String.append가 "oak "와 "tree"를 인자로 받는 함수가 아니라 첫 번째 함수의 인자로 해석되기 때문입니다. 안쪽 String.append 호출의 값을 먼저 구해야 하며, 그런 다음 그 값을 "great " 뒤에 이어 붙여 최종 값 "great oak tree"를 얻습니다.

명령형 언어에는 흔히 두 종류의 조건 구문이 있습니다. 불리언 값에 따라 어떤 명령을 실행할지 결정하는 조건 문과, 불리언 값에 따라 두 표현식 중 어느 것을 평가할지 결정하는 조건 표현식입니다. 예를 들어 C와 C++에서 조건문은 if와 else를 사용해 작성하고, 조건 표현식은 ?와 :가 조건과 분기를 구분하는 삼항 연산자로 작성합니다. Python에서 조건문은 if로 시작하고, 조건 표현식은 if를 가운데에 둡니다. Lean은 표현식 중심의 함수형 언어이므로 조건문은 없고 조건 표현식만 있습니다. 조건 표현식은 if, then, else를 사용해 작성합니다. 예를 들어,

String.append "it is " (if 1 > 2 then "yes" else "no")

다음으로 평가됩니다

String.append "it is " (if false then "yes" else "no")

이는 다음과 같이 평가됩니다

String.append "it is " "no"

이는 최종적으로 "it is no"로 평가됩니다.

간결하게 나타내기 위해, 이와 같은 일련의 평가 단계를 단계 사이에 화살표를 넣어 표기하기도 합니다:

Could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type
  String → String