Lean
Lean
Über LeanÜben

Willst du Lean lernen und meistern?

Komm zum Lean-Track von Exercism und erhalte Zugang zu 100 Übungen mit automatischer Analyse deines Codes und persönlichem Mentoring, alles 100 % kostenlos.

Tritt dem Lean-Track bei Übungen entdecken

Über 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 Programmierübungen für Lean bei Exercism. Von Differenz der Quadrate bis Zwei Eimer.

Werde besser im Programmieren mit unterhaltsamen, lohnenden Programmierübungen bei Exercism, die dein Verständnis von Konzepten auf die Probe stellen.

Differenz der Quadrate

Differenz der Quadrate

Finde die Differenz zwischen dem Quadrat der Summe und der Summe der Quadrate der ersten N natürlichen Zahlen.

Eigene Menge

Eigene Menge

Erstelle einen eigenen Mengentyp.

Zwei Eimer

Zwei Eimer

Zeige mit zwei unterschiedlich großen Eimern, wie man eine exakte Anzahl Liter abmisst.

Alle Lean-Übungen bei Exercism ansehen

Hauptmerkmale von Lean

Lean

Rein funktional

Deterministische Funktionen machen Code vorhersehbar, komponierbar und leichter verständlich.

Abhängig typisiert

Wenn du Regeln direkt in Typen kodierst, dokumentieren sie sich selbst und ungültige Zustände lassen sich nicht darstellen.

Programme und Beweise

Schreibe Programme und beweise ihre Korrektheit in derselben Sprache. Die Spezifikation ist Code.

Bewiesene Korrektheit

Geh über das Testen hinaus und beweise kritische Eigenschaften deines Codes mathematisch.

Typklassen

Typen in Klassen einzuteilen bietet eine leichtgewichtige, erweiterbare Abstraktion.

Starke Metaprogrammierung

Ein mächtiges Makro- und Elaborator-Framework lässt dich die Sprache an deine Domäne anpassen.

Mentoring auf Lean-Art

Jede Sprache hat ihre eigene Art, die Dinge anzugehen. Lean ist da keine Ausnahme. Unsere Mentorinnen und Mentoren helfen dir, wie ein Lean-Entwickler zu denken und idiomatischen Code in Lean zu schreiben. Wenn du eine Übung gelöst hast, reiche sie unserem Freiwilligenteam ein. Es gibt dir Hinweise, Ideen und Feedback dazu, wie du die Übung so gestaltest, wie man es in Lean normalerweise sieht. So hilft es dir, Dinge zu entdecken, von denen du nicht weißt, dass du sie nicht weißt.

Mehr über Mentoring erfahren

Übungen aus der Community für Lean

Der Lean-Track auf Exercism hat 100 Übungen, mit denen du besseren Code schreibst.

Alle Lean-Übungen ansehen
Lean

Leg mit dem Lean-Track los

Das Beste: Es ist für alle zu 100 % kostenlos.

Tritt dem Lean-Track bei