Lean: Log

• Log: rfl proves equations, decide proves decidable propositions
  2026-10-01 · Ryan Williams
  LeanLean: Log

  Both of these close 2 + 2 = 4:

  example : 2 + 2 = 4 := rfl example : 2 + 2 = 4 := by⊢ 2 + 2 = 4 decideAll goals completed! 🐙

  So I assumed they were interchangeable for small closed facts. They are not. rfl fails on 10 < 20:

  example : 10 < 20 := Type mismatch rfl has type ?m.9 = ?m.9 but is expected to have type 10 < 20rfl