Основы

• Синтаксис
• Функции
  • Лямбда-исчисление
  • Мир безымынных функций
  • Упражнения
• Логика
  • Импликация
  • Квантор всеобщности
  • Конъюнкция и дизъюнкция
  • Отрицание
  • Квантор существования
  • Принцип исключённого третьего
  • Логика первого порядка
• Исчисление построений
  • Свойства
  • Зависимые функции
  • Исчисление построений
  • Индуктивные типы
    • Двоичные деревья
    • Деревья бесконечной ширины
    • Парадоксальный индуктивный тип
    • Списки
  • Исчисление индуктивных построений
• Lean
  • Установка
  • Основы Lean
  • Упражнения
  • Равенство