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 Ataque de la reina hasta Apretón de manos secreto.

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

Ataque de la reina

Ataque de la reina

Dadas las posiciones de dos reinas en un tablero de ajedrez, indica si están colocadas de forma que puedan atacarse entre sí.

Trío de colores de resistencia

Trío de colores de resistencia

Convertir los códigos de color que se usan en las resistencias en una etiqueta legible para las personas.

Apretón de manos secreto

Apretón de manos secreto

Dado un número decimal, conviértelo en la secuencia de eventos correspondiente para un apretón de manos secreto.

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