Lean 설치하기🔗

Lean으로 프로그램을 작성하고 실행하려면 먼저 자신의 컴퓨터에 Lean을 설치해야 합니다. Lean 도구 모음은 다음과 같이 구성됩니다.

• elan은 rustup이나 ghcup과 비슷하게 Lean 컴파일러 툴체인을 관리합니다.

• lake는 cargo, make, Gradle과 마찬가지로 Lean 패키지와 그 의존성을 빌드합니다.

• lean은 개별 Lean 파일을 타입 검사하고 컴파일할 뿐만 아니라, 현재 작성 중인 파일에 대한 정보를 프로그래머 도구에 제공합니다. 일반적으로 lean은 사용자가 직접 호출하기보다는 다른 도구가 호출합니다.

• Visual Studio Code나 Emacs 같은 편집기용 플러그인으로, lean과 통신하여 그 정보를 편리하게 보여 줍니다.

Lean 설치에 관한 최신 안내는 Lean 매뉴얼을 참고하십시오.

표기 규칙🔗

Lean에 입력으로 제공되는 코드 예제는 다음과 같은 형식으로 표시됩니다:

위의 마지막 줄(#eval로 시작하는 줄)은 Lean에게 답을 계산하도록 지시하는 명령입니다. Lean의 응답은 다음과 같은 형식으로 표시됩니다.

8

Lean이 반환하는 오류 메시지의 형식은 다음과 같습니다:

Application type mismatch: The argument
  "seven"
has type
  String
but is expected to have type
  Nat
in the application
  add1 "seven"

경고는 다음과 같은 형식으로 표시됩니다:

declaration uses `sorry`

유니코드🔗

관용적인 Lean 코드는 ASCII에 속하지 않는 다양한 유니코드 문자를 사용합니다. 예를 들어, α, β 같은 그리스 문자와 화살표 →는 모두 이 책의 첫 번째 장에 등장합니다. 이를 통해 Lean 코드는 일반적인 수학 표기법에 더 가까운 모습을 띨 수 있습니다.

Lean 기본 설정에서는 Visual Studio Code와 Emacs 모두 백슬래시(\) 뒤에 이름을 붙여 이러한 문자를 입력할 수 있습니다. 예를 들어 α를 입력하려면 \alpha를 입력하십시오. Visual Studio Code에서 어떤 문자를 입력하는 방법을 알아보려면 해당 문자에 마우스를 올려 놓고 툴팁을 확인하십시오. Emacs에서는 해당 문자에 포인트(커서)를 둔 상태에서 C-c C-k를 사용하십시오.

릴리스 이력🔗

저자 소개🔗

David Thrane Christiansen은 20년 동안 함수형 언어를, 10년 동안 의존 타입을 사용해 왔습니다. 그는 Daniel P. Friedman과 함께 의존 타입 이론의 핵심 개념을 소개하는 책인 The Little Typer를 썼습니다. 그는 코펜하겐 IT 대학교에서 박사 학위를 받았습니다. 재학 중에는 Idris 언어의 첫 번째 버전 개발에 주요 기여자로 참여했습니다. 학계를 떠난 뒤에는 오리건주 포틀랜드의 Galois와 덴마크 코펜하겐의 Deon Digital에서 소프트웨어 개발자로 일했으며, Haskell Foundation의 상임 이사(Executive Director)를 역임했습니다. 이 글을 쓰는 시점에 그는 Lean Focused Research Organization에 재직하며 Lean 개발에 전념하고 있습니다.

라이선스🔗

이 책의 원본은 David Thrane Christiansen이 Microsoft Corporation과의 계약에 따라 집필하였으며, Microsoft Corporation은 너그럽게도 이 책을 Creative Commons Attribution 4.0 International License로 공개하였습니다. 현재 버전은 새 버전의 Lean에서 달라진 점을 반영하기 위해 저자가 원본을 수정한 것입니다. 변경 사항에 대한 자세한 설명은 이 책의 소스 코드 저장소에서 확인할 수 있습니다.