Lean
Lean
À propos de LeanEntraînement

Tu veux apprendre et maîtriser Lean ?

Rejoins le parcours Lean d’Exercism pour accéder à 100 exercices avec l'analyse automatique de ton code et un mentorat personnalisé, et tout cela 100 % gratuit.

Rejoins le parcours Lean Explore les exercices

À propos de 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 exercices de programmation pour Lean sur Exercism. De Grep à Duo de couleurs de résistance.

Améliore tes compétences en programmation grâce à des exercices ludiques et gratifiants qui testent ta compréhension des concepts avec Exercism.

Grep

Grep

Rechercher dans un fichier les lignes qui correspondent à un motif d'expression régulière.

Camicia

Camicia

Simule le jeu de cartes et détermine si la partie se termine ou entre dans une boucle infinie.

Duo de couleurs de résistance

Duo de couleurs de résistance

Convertir les codes couleur utilisés sur les résistances en une valeur numérique.

Voir tous les exercices Lean sur Exercism

Les fonctionnalités clés de Lean

Lean

Purement fonctionnel

Les fonctions déterministes rendent le code prévisible, composable et plus facile à comprendre.

Typage dépendant

Encoder les règles directement dans les types rend le code auto-documenté et les états invalides impossibles à représenter.

Programmes et preuves

Écris des programmes et prouve-les corrects dans le même langage. La spécification, c'est du code.

Correction prouvée

Va au-delà des tests en prouvant mathématiquement les propriétés critiques de ton code.

Classes de types

Répartir les types en classes offre une abstraction légère et extensible.

Métaprogrammation puissante

Un _framework_ puissant de macros et d'élaborateurs te permet d'étendre le langage pour l'adapter à ton domaine.

Un mentorat à la manière de Lean

Chaque langage a sa propre façon de faire les choses. Lean ne fait pas exception. Nos mentors t'aideront à apprendre à penser comme un développeur Lean et à écrire du code idiomatique en Lean. Une fois que tu as résolu un exercice, soumets-le à notre équipe de bénévoles, qui te donnera des indices, des idées et des retours sur la façon de le rapprocher de ce que tu verrais habituellement en Lean. Ils t'aideront ainsi à découvrir les choses que tu ne sais pas que tu ne sais pas.

En savoir plus sur le mentorat

Des exercices Lean issus de la communauté

Le parcours Lean sur Exercism propose 100 exercices pour t'aider à écrire du code de meilleure qualité.

Voir tous les exercices Lean
Lean

Lance-toi dans le parcours Lean

Le meilleur, c'est que c'est 100 % gratuit pour tout le monde.

Rejoins le parcours Lean