Lean
Lean
Lean 소개연습

Lean 트랙을 배우고 제대로 익혀 볼까요?

Exercism의 Lean 트랙에 참여해서 100개의 연습 문제와 코드 자동 분석, 그리고 개인 멘토링까지 모두 100% 무료로 이용할 수 있어요.

Lean 트랙 참여하기 연습 문제 살펴보기

Lean 소개

namespace HelloWorld

inductive World where
    | earth | mars

def hello (world : World) : String :=
    match world with
    | .earth => "Hello, Earth!"
    | .mars  => "Hi, Mars!"

end HelloWorld

Exercism의 Lean 트랙을 위한 100개의 코딩 연습 문제 도미노부터 전화번호까지.

Exercism에서 재미있고 보람찬 코딩 연습 문제로 개념에 대한 이해를 확인하며 프로그래밍 실력을 키워 보세요.

도미노

도미노

도미노를 이어서 하나의 사슬을 만들어요.

DOT DSL

DOT DSL

Graphviz의 dot 언어와 비슷한 도메인 특화 언어를 작성해요.

전화번호

전화번호

사용자가 입력한 전화번호를 정리해서 SMS 메시지를 보낼 수 있게 해요.

Exercism에서 Lean 연습 문제 모두 보기

Lean의 주요 기능

Lean

순수 함수형

결정적인 함수 덕분에 코드는 예측 가능하고 조합하기 쉬우며 이해하기도 쉬워요.

의존 타입

규칙을 타입에 직접 표현하면 타입 자체가 문서가 되고, 잘못된 상태는 표현할 수 없게 돼요.

프로그램과 증명

같은 언어로 프로그램을 작성하고 그 정확성을 증명해요. 명세가 곧 코드예요.

증명된 정확성

코드의 중요한 성질을 수학적으로 증명함으로써 테스트를 넘어설 수 있어요.

타입 클래스

타입을 클래스로 분류하면 가볍고 확장 가능한 추상화를 얻을 수 있어요.

강력한 메타프로그래밍

강력한 매크로와 엘라보레이터 프레임워크로 언어를 자신의 도메인에 맞게 확장할 수 있어요.

Lean 방식으로 멘토링 받기

모든 언어에는 저마다의 방식이 있어요. Lean도 마찬가지예요. 멘토가 Lean 개발자처럼 생각하는 법과 Lean다운 코드를 작성하는 법을 익히도록 도와줘요. 연습 문제를 하나 풀면 자원봉사 팀에 제출해 보세요. 그러면 힌트와 아이디어, 그리고 Lean에서 흔히 볼 수 있는 코드에 더 가깝게 다듬는 방법에 대한 피드백을 받을 수 있어요. 스스로는 알지 못한다는 사실조차 몰랐던 것들을 발견하도록 도와주는 거예요.

멘토링에 대해 더 알아보기

커뮤니티가 함께 만든 Lean 연습 문제

Exercism의 Lean 트랙에는 더 나은 코드를 작성하는 데 도움이 되는 100개의 연습 문제가 있어요.

Lean 연습 문제 모두 보기
Lean

Lean 트랙 시작하기

가장 좋은 점은, 누구에게나 100% 무료라는 거예요.

Lean 트랙 참여하기