refactor: unify ℒₒᵣ/ℒₛₑₜ syntax type aliases#837
Merged
Conversation
…ence`/`SetTheorySentence` Add the `SetTheorySentence := Sentence ℒₛₑₜ` alias to mirror the existing `ArithmeticSentence := Sentence ℒₒᵣ`, and replace bare `Sentence ℒₒᵣ` / `Sentence ℒₛₑₜ` occurrences with the aliases. The extended-language `Sentence ℒₒᵣ⋆` and the alias definitions themselves are left untouched. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Introduce the full set-theory alias family in `SetTheory/Basic/Misc.lean` (`SetTheorySemiformula`, `SetTheoryFormula`, `SetTheorySemisentence`, `SetTheorySemiproposition`, `SetTheoryProposition`), mirroring the existing arithmetic family, and replace bare `Semiformula`/`Formula`/`Semisentence`/ `Sentence`/`Semiproposition`/`Proposition`/`Theory` applied to `ℒₒᵣ`/`ℒₛₑₜ` with the corresponding aliases throughout. Following the current `FirstOrder` redesign (#794), term-level aliases (`Semiterm`/`Term`) are intentionally left bare, as is the extended language `ℒₒᵣ⋆`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…Arithmetic/Basic/Misc.lean` - Add term-level aliases `ArithmeticSemiterm`/`ArithmeticTerm` and `SetTheorySemiterm`/`SetTheoryTerm`, and replace bare `Semiterm`/`Term` applied to `ℒₒᵣ`/`ℒₛₑₜ` with them. - Move the whole arithmetic alias family out of `Basic/Syntax/Formula.lean` into `Arithmetic/Basic/Misc.lean`, mirroring how the set-theory aliases live in `SetTheory/Basic/Misc.lean`. The generic `Semisentence`/`Semiproposition`/ `Proposition` stay in `Formula.lean`. - The lone upstream `#check` in `Basic/BinderNotation.lean` keeps the bare `Semiterm ℒₒᵣ`, since it precedes the alias definitions. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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.
Bare
Sentence ℒₒᵣ/Sentence ℒₛₑₜand their aliases were mixed throughout the codebase, and the set-theory side had almost no aliases at all. This continues #806 (fixing #803), redone on top of the currentmasterand adapted to the presentFirstOrderdesign (#794).Changes
ℒₒᵣandℒₛₑₜ, covering every syntax level:Semiterm/Term/Semiformula/Formula/Semisentence/Sentence/Semiproposition/Proposition/Theory.ArithmeticSemiterm,ArithmeticTerm,ArithmeticSemiformula,ArithmeticFormula,ArithmeticSemisentence,ArithmeticSentence,ArithmeticSemiproposition,ArithmeticProposition,ArithmeticTheory.SetTheorySemiterm,SetTheoryTerm,SetTheorySemiformula,SetTheoryFormula,SetTheorySemisentence,SetTheorySentence,SetTheorySemiproposition,SetTheoryProposition(alongside the existingSetTheory := Theory ℒₛₑₜ).<syntax> ℒₒᵣ/<syntax> ℒₛₑₜoccurrences with the corresponding aliases throughout.FirstOrder/Basic/Syntax/Formula.leanintoFirstOrder/Arithmetic/Basic/Misc.lean, mirroring how the set-theory aliases live inFirstOrder/SetTheory/Basic/Misc.lean. The genericSemisentence/Semiproposition/Proposition(parameterized byL : Language) stay inFormula.lean.Notes
FirstOrder#794), the naming usesSemiproposition/Proposition(not theSyntacticFormulanaming from the original refactor: replaceSentence ℒₒᵣ/Sentence ℒₛₑₜwithArithmeticSentence/SetTheorySentence#806).ℒₒᵣ⋆(TA/Nonstandard.lean) is intentionally left untouched.#checkinBasic/BinderNotation.leankeeps the bareSemiterm ℒₒᵣ, since it precedes the (relocated) alias definitions.Fixes #803
🤖 Generated with Claude Code