Lean
Lean
Acerca de LeanPracticar

¿Quieres aprender y dominar Lean?

Únete a la ruta de Lean de Exercism para acceder a 100 ejercicios con análisis automático de tu código y mentoría personal, todo 100 % gratis.

Únete a la ruta de Lean Explora los ejercicios

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 ejercicios de programación de Lean en Exercism. Desde Año bisiesto hasta Números romanos.

Mejora tu nivel de programación con ejercicios divertidos y gratificantes que ponen a prueba tu comprensión de los conceptos con Exercism.

Año bisiesto

Año bisiesto

Determina si un año dado es bisiesto.

Traducción de proteínas

Traducción de proteínas

Traduce secuencias de ARN en proteínas.

Números romanos

Números romanos

Convierte números árabes modernos en números romanos.

Ver todos los ejercicios de Lean en Exercism

Características clave de Lean

Lean

Puramente funcional

Las funciones deterministas hacen que el código sea predecible, componible y más fácil de entender.

Tipado dependiente

Codificar las reglas directamente en los tipos hace que se autodocumenten y que los estados no válidos no puedan representarse.

Programas y demostraciones

Escribe programas y demuestra que son correctos en el mismo lenguaje. La especificación es código.

Corrección demostrada

Ve más allá de las pruebas demostrando matemáticamente propiedades críticas de tu código.

Clases de tipos

Categorizar los tipos en clases proporciona una abstracción ligera y extensible.

Metaprogramación potente

Un potente marco de macros y elaboradores te permite extender el lenguaje para adaptarlo a tu dominio.

Recibe mentoría al estilo Lean

Cada lenguaje tiene su propia forma de hacer las cosas. Lean no es una excepción. Nuestros mentores te ayudarán a aprender a pensar como un desarrollador de Lean y a escribir código idiomático en Lean. Cuando hayas resuelto un ejercicio, envíalo a nuestro equipo de voluntarios y te darán pistas, ideas y comentarios sobre cómo hacer que se parezca más a lo que normalmente verías en Lean. Te ayudarán a descubrir esas cosas que no sabes que no sabes.

Más información sobre la mentoría

Ejercicios de Lean creados por la comunidad

El track Lean en Exercism tiene 100 ejercicios para ayudarte a escribir mejor código.

Ver todos los ejercicios de Lean
Lean

Empieza con el track Lean

Y lo mejor de todo: es 100% gratis para todo el mundo.

Únete al track Lean