Lean
Lean
Informazioni su LeanFai pratica

Vuoi imparare e padroneggiare Lean?

Unisciti al track Lean di Exercism per accedere a 100 esercizi con l'analisi automatica del codice e mentoring personale, tutto 100% gratuito.

Unisciti al track Lean Esplora gli esercizi

Informazioni su 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 esercizi di programmazione per Lean su Exercism. Da Parsing di SGF a Isogramma.

Migliora nella programmazione con esercizi divertenti e gratificanti che mettono alla prova la tua comprensione dei concetti su Exercism.

Parsing di SGF

Parsing di SGF

Esegui il parsing di una stringa in formato Smart Game Format.

Luhn

Luhn

Dato un numero, determina se è valido o no secondo la formula di Luhn.

Isogramma

Isogramma

Determina se una frase è un isogramma, una parola senza lettere ripetute.

Vedi tutti gli esercizi di Lean su Exercism

Funzionalità principali di Lean

Lean

Puramente funzionale

Le funzioni deterministiche rendono il codice prevedibile, componibile e più facile da capire.

Tipi dipendenti

Codificare le regole direttamente nei tipi le rende autoesplicative e impedisce di rappresentare stati non validi.

Programmi e dimostrazioni

Scrivi programmi e dimostrane la correttezza nello stesso linguaggio. La specifica è codice.

Correttezza dimostrata

Vai oltre i test dimostrando matematicamente le proprietà critiche del codice.

Classi di tipi

Classificare i tipi in classi offre un'astrazione leggera ed estensibile.

Metaprogrammazione potente

Un potente framework di macro ed elaboratori consente di estendere il linguaggio ed adattarlo al tuo dominio.

Ricevi mentoring nello stile di Lean

Ogni linguaggio ha il suo modo di fare le cose. La traccia Lean non fa eccezione. I nostri mentori ti aiuteranno a imparare a pensare come uno sviluppatore Lean e a scrivere codice idiomatico in Lean. Dopo aver risolto un esercizio, invialo alla nostra squadra di volontari, che ti darà suggerimenti, idee e feedback su come renderlo più simile a quello che vedresti normalmente in Lean: ti aiuteranno a scoprire le cose che non sai di non sapere.

Scopri di più sul mentoring

Esercizi Lean creati dalla community

La traccia Lean su Exercism ha 100 esercizi per aiutarti a scrivere codice migliore.

Vedi tutti gli esercizi di Lean
Lean

Inizia con la traccia Lean

La parte migliore: è gratis al 100% per tutti.

Unisciti alla traccia Lean