Skip to content

refactor: fix Kreisel spelling throughout codebase#773

Merged
SnO2WMaN merged 4 commits into
masterfrom
copilot/fix-kriesel-to-kreisel
Feb 20, 2026
Merged

refactor: fix Kreisel spelling throughout codebase#773
SnO2WMaN merged 4 commits into
masterfrom
copilot/fix-kriesel-to-kreisel

Conversation

Copilot AI commented Feb 20, 2026

Copy link
Copy Markdown
Contributor

Every occurrence of the misspelling "Kriesel" (as in Georg Kreisel) has been corrected to "Kreisel". This includes a secondary variant "Krisel" (missing 'e') found in SatisfiesKriselPutnamCondition.

Changes

  • File renames:

    • Entailment/KrieselPutnam.leanKreiselPutnam.lean
    • Kripke/AxiomKrieselPutnam.leanAxiomKreiselPutnam.lean
    • Kripke/Logic/KrieselPutnam.leanKreiselPutnam.lean
  • Identifier/name renames across 7 files:

    • HasAxiomKrieselPutnamHasAxiomKreiselPutnam
    • HasKrieselPutnamHasKreiselPutnam
    • SatisfiesKriselPutnamConditionSatisfiesKreiselPutnamCondition
    • kriesel_putnam / krieselputnamkreisel_putnam / kreiselputnam
    • kriesel_remarkkreisel_remark (in FirstOrder/Bootstrapping)
    • All import paths updated accordingly
Original prompt

This section details on the original issue you should resolve

<issue_title>Fix Kriesel to Kreisel</issue_title>
<issue_description>Rename every misspelling Kriesel to Kriesel. </issue_description>

Comments on the Issue (you are @copilot in this section)


💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.

Co-authored-by: SnO2WMaN <15155608+SnO2WMaN@users.noreply.github.com>
Copilot AI changed the title [WIP] Fix spelling of Kriesel to Kreisel Fix Kreisel spelling throughout codebase Feb 20, 2026
Copilot AI requested a review from SnO2WMaN February 20, 2026 11:22
@SnO2WMaN

Copy link
Copy Markdown
Member

@copilot

Update commit message

@SnO2WMaN SnO2WMaN marked this pull request as ready for review February 20, 2026 12:06

Copilot AI commented Feb 20, 2026

Copy link
Copy Markdown
Contributor Author

@copilot

Update commit message

Based on the conventional commit format in CONTRIBUTING.md, the PR title (which becomes the squash-merge commit message) should be:

refactor: fix Kreisel spelling throughout codebase

Using refactor since this is purely a rename/reorganization with no change to existing results.

@SnO2WMaN SnO2WMaN changed the title Fix Kreisel spelling throughout codebase refactor: fix Kreisel spelling throughout codebase Feb 20, 2026
@SnO2WMaN SnO2WMaN enabled auto-merge (squash) February 20, 2026 12:08
@SnO2WMaN SnO2WMaN merged commit 8c5b27c into master Feb 20, 2026
5 checks passed
@SnO2WMaN SnO2WMaN deleted the copilot/fix-kriesel-to-kreisel branch February 20, 2026 12:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Fix _Kriesel_ to _Kreisel_

2 participants