tests: add orphan-rec and orphan-ctor - #158
Merged
Merged
Conversation
Two hand-written exports in which a bogus declaration escapes checking by not being attached to any inductive declaration, rather than by disagreeing with one: * orphan-rec: a second recursor `rogue : False` in `False`'s inductive block whose `all` field is empty, so a checker that requires the recursors naming an inductive type to be exactly the derived ones never looks at it. This is the sibling of extra-rec that defeats the obvious fix for it; nanoda accepted it until ammkrn/nanoda_lib@8a327a1. * orphan-ctor: a constructor `rogue : False` in `False`'s inductive block (which keeps `ctors: []`) whose `induct` field names a declaration that does not exist in the export. Both are written by hand because lean4export cannot produce them: it collects an inductive block's recursors from the `all` fields of the recursors and its constructors from the inductive's `ctors` field, so either orphan is silently dropped. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01SbJDfxpQcw7Zh4LF9YZzNP
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Two hand-written exports in which a bogus declaration escapes checking by
not being attached to any inductive declaration, rather than by
disagreeing with one:
orphan-rec: a second recursor
rogue : FalseinFalse's inductiveblock whose
allfield is empty, so a checker that requires therecursors naming an inductive type to be exactly the derived ones never
looks at it. This is the sibling of extra-rec that defeats the obvious
fix for it; nanoda accepted it until ammkrn/nanoda_lib@8a327a1.
orphan-ctor: a constructor
rogue : FalseinFalse's inductive block(which keeps
ctors: []) whoseinductfield names a declaration thatdoes not exist in the export.
Both are written by hand because lean4export cannot produce them: it
collects an inductive block's recursors from the
allfields of therecursors and its constructors from the inductive's
ctorsfield, soeither orphan is silently dropped.
Co-Authored-By: Claude Opus 5 (1M context) noreply@anthropic.com
Claude-Session: https://claude.ai/code/session_01SbJDfxpQcw7Zh4LF9YZzNP