Conversation
|
Thanks for contributing to Lem, but really - if there's a large codebase with trailing whitespaces, you can safely assume (a) that we're fine with that, and also (b) that it's likely no-one really has time to check over a big diff for no benefit. Our available resource for maintaining Lem is unfortunately quite limited. |
|
Didn't wan't to remove them for no reason. When fixing real stuff (e.g. #6), it's a pain when your editor remove them automatically on save, you have to cancel everything, use another editor or change your preferences etc. Or just keep these changes, which will make the diff really hard to read... (e.g. #6 again). (Plus, you can check this PR is harmless by just cloning my fork, building on the correct branch, comparing the binaries. It just take 5 minutes and a few commands. Or just believing me. But I understand you have limited time...) |
…FixedPoint Convert 5 more partial defs to total: - LemLib.lean: boolListFromNatural (n/2 division), bitSeqBinopAux (dual-list recursion) - LemLib.lean: lemStringFromNatHelper, lemStringFromNaturalHelper (n/10 division) - LemLib.lean: lemLeastFixedPoint (bounded countdown) Add Lean-only target reps in string_extra.lem and set.lem to route generated code through the total LemLib implementations. All changes are inherently Lean-scoped (declare lean target_rep / hand-written Lean). Add TODO rems-project#7: audit all pre-existing unscoped termination annotations from upstream to verify they don't affect other backends. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
2 participants
Hi,
Just removed trailing-whitespaces.