Lean
Lean
Про LeanПрактика

Хочемо вивчити й опанувати Lean?

Приєднаймося до треку Lean на Exercism, щоб отримати доступ до 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

100 вправ із програмування для Lean на Exercism. Від вправи Grep до вправи Luhn.

Удосконалюймо навички програмування завдяки цікавим і корисним вправам, які перевіряють наше розуміння концепцій на Exercism.

Grep

Grep

Знайдіть у файлі рядки, що збігаються з регулярним виразом.

Обертальний шифр

Обертальний шифр

Створіть реалізацію обертального шифру, який також іноді називають шифром Цезаря.

Luhn

Luhn

Дано число; визначте, чи воно чинне за формулою Луна.

Переглянути всі вправи Lean на Exercism

Ключові можливості Lean

Lean

Чисто функціональна

Детерміновані функції роблять код передбачуваним, легким для композиції та зрозумілішим.

Залежні типи

Коли правила закодовано безпосередньо в типах, вони самі себе документують, а некоректні стани стають неможливими.

Програми й доведення

Пишемо програми й доводимо їхню правильність тією самою мовою. Специфікація - це код.

Доведена правильність

Не обмежуймося тестуванням: математично доводьмо критичні властивості свого коду.

Класи типів

Групування типів у класи забезпечує легку й розширювану абстракцію.

Потужне метапрограмування

Потужний фреймворк макросів та елабораторів дає змогу розширити мову під конкретну предметну область.

Наставництво у стилі Lean

У кожної мови свої звичаї. Lean не виняток. Наші наставники допоможуть нам навчитися думати як розробник Lean і писати ідіоматичний код мовою Lean. Коли ми розвʼяжемо вправу, надішлімо її нашій команді волонтерів, і вони дадуть нам підказки, ідеї та відгук про те, як зробити її ближчою до того, що ми зазвичай бачимо мовою Lean, і допоможуть нам відкрити те, чого ми не знаємо, що не знаємо.

Дізнатися більше про наставництво

Вправи Lean від спільноти

Трек Lean на Exercism має 100 вправ, щоб допомогти нам писати кращий код.

Переглянути всі вправи Lean
Lean

Почати з треку Lean

А найкраще те, що це 100% безкоштовно для всіх.

Приєднайтеся до треку Lean