Lean
Lean
Acerca de LeanPracticar

¿Quieres aprender y dominar Lean?

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

Únete al track de Lean Explora los ejercicios

Acerca de 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 Era espacial hasta Números de Armstrong.

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

Era espacial

Era espacial

Dada una edad en segundos, calcula cuántos años tiene alguien en años solares de un planeta dado.

Búsqueda binaria

Búsqueda binaria

Implementa un algoritmo de búsqueda binaria.

Números de Armstrong

Números de Armstrong

Determina si un número es un número de Armstrong.

Ver todos los ejercicios de Lean en Exercism

Características principales de Lean

Lean

Puramente funcional

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

Con tipos dependientes

Codificar las reglas directamente en los tipos los hace autodocumentados y hace imposible representar estados inválidos.

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 y demuestra 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 framework de macros y elaboración te permite extender el lenguaje para que se adapte a tu dominio.

Recibe mentoría al estilo de Lean

Cada lenguaje tiene su propia forma de hacer las cosas. Lean no es la 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 lograr 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.

Aprende más sobre la mentoría

Ejercicios de Lean creados por la comunidad

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

Ver todos los ejercicios de Lean
Lean

Empieza con el track de Lean

Lo mejor de todo: es 100% gratis para todos.

Únete al track de Lean