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.
namespace HelloWorld
inductive World where
| earth | mars
def hello (world : World) : String :=
match world with
| .earth => "Hello, Earth!"
| .mars => "Hi, Mars!"
end HelloWorld
Melhore suas habilidades de programação com exercícios divertidos e gratificantes que testam sua compreensão dos conceitos no Exercism.
Encontre as palavras que usam as mesmas letras que outra palavra.
Implemente as operações `keep` e `discard` em coleções.
Dado um ano, determine se ele é bissexto.
Funções determinísticas tornam o código previsível, componível e mais fácil de entender.
Codificar regras diretamente nos tipos faz com que eles se autodocumentem e torna estados inválidos irrepresentáveis.
Escreva programas e prove que estão corretos na mesma linguagem. A especificação é código.
Vá além dos testes provando matematicamente propriedades críticas do seu código.
Categorizar tipos em classes oferece uma abstração leve e extensível.
Um poderoso framework de macros e elaboradores permite estender a linguagem para se adequar ao seu domínio.
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 mentoriaA trilha de Lean no Exercism tem 100 exercícios para ajudar você a escrever código melhor.
Ver todos os exercícios de LeanE o melhor de tudo: é 100% grátis para todo mundo.
Entre na trilha de Lean