Quer aprender e dominar Lean?

Junte-se à Trilha Lean do Exercism e tenha acesso a 100 exercícios com análise automática do seu código e mentoria pessoal, tudo 100% grátis.

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 Anagrama a Ano Bissexto.


Melhore suas habilidades de programação com exercícios divertidos e gratificantes que testam sua compreensão dos conceitos no Exercism.

Ver todos os exercícios de Lean no Exercism

Principais recursos de Lean


Lean

Puramente funcional

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

Tipagem dependente

Codificar regras diretamente nos tipos faz com que eles se autodocumentem e torna estados inválidos irrepresentáveis.

Programas e provas

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

Correção provada

Vá além dos testes provando matematicamente propriedades críticas do seu código.

Classes de tipos

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

Metaprogramação poderosa

Um poderoso framework de macros e elaboradores permite estender a linguagem para se adequar ao seu domínio.

Receba mentoria no estilo Lean

Toda linguagem tem o seu próprio jeito de fazer as coisas. Com Lean não é diferente. Nossos mentores vão ajudar você a aprender a pensar como um desenvolvedor de Lean e a escrever código idiomático em Lean. Depois de resolver um exercício, envie-o para a nossa equipe de voluntários, e eles vão dar dicas, ideias e feedback sobre como deixá-lo mais parecido com o que você normalmente veria em Lean. Eles vão ajudar você a descobrir as coisas que você não sabe que não sabe.

Saiba mais sobre mentoria

Exercícios de Lean criados pela comunidade

A trilha de Lean no Exercism tem 100 exercícios para ajudar você a escrever código melhor.

Ver todos os exercícios de Lean
Lean

Comece agora na trilha de Lean

E o melhor de tudo: é 100% grátis para todo mundo.

Entre na trilha de Lean