Lean
Lean
Sobre LeanPraticar

Queres aprender e dominar Lean?

Junta-te ao Percurso de Lean do Exercism para teres acesso a 100 exercícios com análise automática do teu código e mentoria pessoal, tudo 100% gratuito.

Junta-te ao Percurso de Lean Explora os exercícios

Sobre 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 exercícios de programação de Lean no Exercism. De Dois Baldes a Quantidade de Comprimento Variável.

Torna-te melhor a programar com exercícios divertidos e gratificantes que põem à prova a tua compreensão dos conceitos no Exercism.

Dois Baldes

Dois Baldes

Dados dois baldes de tamanhos diferentes, demonstra como medir uma quantidade exata de litros.

Fatores primos

Fatores primos

Calcula os fatores primos de um número natural dado.

Quantidade de Comprimento Variável

Quantidade de Comprimento Variável

Implementa a codificação e a descodificação de quantidades de comprimento variável.

Vê todos os exercícios de Lean no Exercism

Funcionalidades principais de Lean

Lean

Puramente funcional

As funções determinísticas tornam o código previsível, componível e mais fácil de compreender.

Com tipos dependentes

Codificar regras diretamente nos tipos torna-as autoexplicativas e impede que existam estados inválidos.

Programas e provas

Escreve programas e prova que estão corretos na mesma linguagem. A especificação é código.

Correção provada

Vai além dos testes ao provar matematicamente propriedades críticas do teu código.

Classes de tipos

Categorizar tipos em classes proporciona uma abstração leve e extensível.

Metaprogramação poderosa

Uma poderosa estrutura de macros e de elaboradores permite-te estender a linguagem às necessidades do teu domínio.

Recebe mentoria ao estilo de Lean

Cada linguagem tem a sua própria forma de fazer as coisas. Lean não é exceção. Os nossos mentores vão ajudar-te a aprender a pensar como um programador de Lean e a escrever código idiomático em Lean. Depois de resolveres um exercício, submete-o à nossa equipa de voluntários e eles darão dicas, ideias e feedback sobre como fazer com que o teu código se pareça mais com aquilo que costumas ver em Lean. Vão ajudar-te a descobrir as coisas que não sabes que não sabes.

Sabe mais sobre mentoria

Exercícios de Lean criados pela comunidade

O percurso Lean do Exercism tem 100 exercícios para te ajudar a escrever melhor código.

Vê todos os exercícios de Lean
Lean

Começa com o percurso Lean

A melhor parte: é 100% gratuito para todos.

Junta-te ao percurso Lean