Lean Kernel Arena / tutorial/073_BogusRecursor

A kernel must not blindly trust the recursors it is handed. If we write

inductive BogusRecursor : Type where
  | mk : BogusRecursor

then the recursor BogusRecursor.rec will be correctly derived with type {motive : BogusRecursor → Sort u} → motive .mk → (t : BogusRecursor) → motive t.

This test instead claims that the recursor is a constant of type False, and then uses it to prove bogusRecursorFalse : False. A kernel that validates the recursors it is handed rejects the bogus recursor itself; a kernel that ignores them and derives the recursors anew rejects the proof of False (the derived recursor neither has type False nor zero universe parameters). Either way, this test must be rejected.