Preámbulo

Lean desde cero

El lenguaje en la práctica: expresiones, tipos, funciones y pruebas construidas una a una, hasta leer un teorema real de la tesis.

Adaptado de: Preámbulo: preparación para leer la tesis.

Contenido

1. Lean es una calculadora que juzga
2. fun: la función anónima
3. Varias variables: currificación
4. Tipos que se construyen
5. Prop: cuando el tipo es una afirmación
6. Demostrar es programar
7. Tácticas: el modo interactivo
8. Ya puedes leer la tesis