Lean: Log

Part of Lean from the Inside. Follow the series in reading order or explore the entries below.

• Log: rfl proves equations, decide proves decidable propositions
  2026-10-01

  A small experiment in the difference between definitional equality and decidable propositions.

  LeanLean: Log