Getting Lean🔗

Lean으로 작성한 프로그램을 쓰고 실행하기 전에 자신의 컴퓨터에 Lean을 설치해야 한다. Lean 도구는 다음으로 구성된다.

• elan은 rustup이나 ghcup처럼 Lean 컴파일러 툴체인을 관리한다.

• lake는 cargo, make, Gradle처럼 Lean 패키지와 의존성을 빌드한다.

• lean은 개별 Lean 파일의 타입을 검사하고 컴파일하며 현재 작성 중인 파일에 대한 정보를 프로그래머 도구에 제공한다. 보통 사용자가 직접 실행하기보다 다른 도구가 lean을 호출한다.

• Visual Studio Code나 Emacs 같은 편집기 플러그인은 lean과 통신하고 그 정보를 편리하게 표시한다.

최신 Lean 설치 방법은 Lean 매뉴얼을 참고하라.

Typographical Conventions🔗

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`

Unicode🔗

관용적인 Lean 코드는 ASCII에 속하지 않는 다양한 유니코드 문자를 사용한다. 예를 들어 이 책의 첫 장에는 α, β 같은 그리스 문자와 화살표 →가 나온다. 덕분에 Lean 코드는 일반적인 수학 표기와 더 비슷해진다.

기본 Lean 설정에서는 Visual Studio Code와 Emacs 모두 백슬래시(\) 뒤에 이름을 입력해 이러한 문자를 쓸 수 있다. 예를 들어 α를 입력하려면 \alpha를 입력하라. Visual Studio Code에서 문자를 입력하는 방법을 알려면 해당 문자 위에 마우스를 올리고 도구 설명을 확인하라. Emacs에서는 해당 문자에 포인트를 둔 채 C-c C-k를 사용하라.

Release history🔗

About the Author🔗

David Thrane Christiansen은 20년 동안 함수형 언어를, 10년 동안 종속 타입을 사용해 왔다. Daniel P. Friedman과 함께 종속 타입 이론의 핵심 아이디어를 소개하는 The Little Typer를 썼다. 코펜하겐 IT 대학교에서 박사 학위를 받았다. 학업 중 Idris 언어의 첫 버전에 크게 기여했다. 학계를 떠난 뒤 오리건주 포틀랜드의 Galois와 덴마크 코펜하겐의 Deon Digital에서 소프트웨어 개발자로 일했으며 Haskell Foundation의 사무총장을 지냈다. 집필 당시에는 Lean Focused Research Organization에서 Lean 전업 개발자로 근무하고 있다.

License🔗

이 책의 원본은 David Thrane Christiansen이 Microsoft Corporation과의 계약으로 작성했으며, Microsoft는 이를 Creative Commons Attribution 4.0 International License로 아낌없이 공개했다. 현재 버전은 최신 Lean 버전의 변경을 반영하도록 저자가 원본에서 수정했다. 변경 사항의 자세한 기록은 책의 소스 코드 저장소에서 확인할 수 있다.