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"를 얻을 수 있습니다.

명령형 언어에는 흔히 두 종류의 조건문이 있는데, 불리언 값에 따라 어떤 명령을 실행할지 결정하는 조건 문(statement)과 불리언 값에 따라 두 표현식 중 어느 것을 평가할지 결정하는 조건 표현식(expression)이 그것입니다. 예를 들어, 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