fix(a2ml): complete normative core verification - #621
Merged
Conversation
Close the remaining standards#556 gaps by making every converter renderer structurally total, including Converters in the authoritative package, and replacing the per-file false-green CI checks with an ipkg typecheck. Verified with Idris2 0.7.0, just validate, the full 25-file shell suite, and git diff --check.
|
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.
Summary
Closes #556.
List BlockData.Maybeimports and remove the converter's accidentalEq RefrequirementA2ML.Convertersin the normativea2ml-core.ipkgidris2 --checkcalls with the real package gate:idris2 --typecheck a2ml-core.ipkgNo
postulate,believe_me,assert_total, or new partial renderer was introduced.Verification
idris2 --source-dir src --check src/A2ML/Converters.idrpassedidris2 --typecheck a2ml-core.ipkgpassed with all 11 package modulesjust validatepassedgit diff --checkpassedContext
The parser and first ten package modules were repaired in #567. This PR completes the two deliberately deferred items documented there and on #556: the converter restructure and a non-vacuous package-level CI gate.