Nivel 6

El CIC y Lean

Tipos inductivos, recursores y eliminadores: el cálculo que Lean implementa, y las tácticas como constructores de términos.

Adaptado de: Capítulo: Cálculo de Construcciones Inductivas.

Contenido

1. El CoC puro y sus límites
2. Tipos inductivos
3. Recursores y eliminación
4. Prop, Type y universos
5. Tácticas: metaprogramas sobre el CIC