Resumen de lecturas compartidas durante octubre de 2020

Esta entrada es una recopilación de lecturas compartidas, durante octubre de 2020, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.

Las lecturas están ordenadas según su fecha de publicación en Twitter.

Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.

Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Read More “Resumen de lecturas compartidas durante octubre de 2020”

ForMatUS: Pruebas en Lean de una desigualdad entre números naturales

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 8 pruebas en Lean de una desigualdad entre números naturales, usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada