ForMatUS: Conectivas y desigualdades en Lean

PorJosé A. Alonso

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo Conectivas y desigualdades en Lean en el se comentan las demostraciones en Lean de algunas de las propiedades de las desigualdades de los números reales estudiadas en vídeos anteriores, pero formuladas con conectivas. Concretamente, se demuestran las 5 propiedades siguientes:

Sean a, b y c números reales.

  1. 0 ≤ a → b ≤ a + b
  2. 0 ≤ b → a ≤ a + b
  3. (0 ≤ a ∧ 0 ≤ b) → 0 ≤ a + b
  4. 0 ≤ a → (0 ≤ b → 0 ≤ a + b)
  5. Si (0 ≤ a ∧ 0 ≤ b) → 0 ≤ a + b, entonces 0 ≤ a → (0 ≤ b → 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

PFH: Definiciones por recursión en Haskell (Parte 2 de 2)

PorJosé A. Alonso

He añadido a la lista Programación funcional con Haskell el vídeo Definiciones por recursión en Haskell (Parte 2 de 2) en el que se completa el estudio de las definiciones por recursión en Haskell comenzado en el vídeo anterior. Concretamente, hemos visto ejemplos de

  • recursión sobre varios argumento,
  • recursión múltiple y
  • de recursión mutua.

El vídeo es

Los apuntes correspondientes son

Una versión interactiva de los apuntes en IHaskell se encuentra aquí.

PFH: Definiciones por recursión en Haskell (Parte 1 de 2)

PorJosé A. Alonso

He añadido a la lista Programación funcional con Haskell el vídeo Definiciones por recursión en Haskell (Parte 1 de 2) en el que se e,pieza el estudio de las definiciones por recursión en Haskell. Concretamente, hemos visto ejemplos de

  • recursión sobre los números naturales y
  • recursión sobre listas.

El vídeo es

Los apuntes correspondientes son

Una versión interactiva de los apuntes en IHaskell se encuentra aquí.