Lean Kernel Arena / orphan-rec

Proof of False from a recursor that claims not to belong to any inductive type.

The export contains False exactly as the prelude has it — an empty Prop-valued inductive with no constructors — together with its ordinary False.rec. Smuggled into the same inductive block is a second recursor, named rogue, whose type is False itself, which has no motives, no minor premises and no rules, and whose all field is the empty list. The theorem inconsistent : False is then simply rogue.

This is the sibling of extra-rec, and it defeats the obvious fix for it. A checker that associates each exported recursor with the inductive type named in its all field, and then requires the recursors so associated with an inductive type to be exactly the ones it derives from that declaration, still accepts rogue: False is associated with False.rec and nothing else, and rogue is associated with nothing at all, so no comparison ever looks at it — yet it is added to the environment and inhabits the genuine empty type.

A checker must therefore reject any recursor it did not itself derive from an inductive declaration, rather than only checking the recursors that point at one. The same hole is reachable by pointing all at a name that has no declaration in the export (that variant is what orphan-ctor does on the constructor side).

Nanoda accepted this export until it was fixed.