He añadido a la lista Programación funcional con Haskell el vídeo Cifrado César en Haskell en el que se estudia cómo definir en Haskell la codificación de mensajes usando el cifrado César.
El vídeo es
Los apuntes correspondientes son
Una versión interactiva de los apuntes en IHaskell se encuentra aquí.
En el vídeo se comentan 5 demostraciones en Lean de la siguiente propiedad:
Sean a, b y c números reales. Si c ≤ 0 y a ≤ b, entonces bc ≤ ac.
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo
En el vídeo se comentan 6 demostraciones en Lean de la siguiente propiedad:
Sean a, b y c números reales. Si 0 ≤ c y a ≤ b, entonces ac ≤ bc.
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo
En el vídeo se comentan distintas pruebas en Lean de la siguiente propiedad:
Sean a, b, c y d números reales. Si a ≤ b y c ≤ d, entonces a + c ≤ b + d.
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo
En el vídeo se comentan distintas pruebas en Lean de la siguiente propiedad:
Sean a y b números reales. Si 0 ≤ a y 0 ≤ b, entonces 0 ≤ a + b.
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo