Commit 2024-09-06 08:34 cf412fcd

View on Github →

refactor(ModelTheory): Remove FirstOrder.Language.mk₂ and related constructors (#16369) Redefines FirstOrder.Language.constantsOn to not use FirstOrder.Language.mk₂ Removes FirstOrder.Language.mk₂ and related constructors, and lemmas about them These constructors were set up to define first-order languages and structures with symbols of at most binary arity. While they provided a unifying framework for constructing all specific examples of first-order languages in mathlib so far, working with them was not as simple (at least in Lean4) as defining the function and relation symbol type sequences (of type ℕ → Type u) as inductives, as seen first with FirstOrder.Language.ring. Once the last use case of these constructors, FirstOrder.Language.constantsOn, turned out to be at least as easy to define and work with without the constructors, there seems to be no remaining reason to keep them around. Their main advantage was that they required relatively little knowledge of Lean syntax to use, but now there are several examples of inductive FirstOrder.Language definitions to use as templates. Deletions:

  • FirstOrder.Language.RelMap₂
  • FirstOrder.Language.Sequence₂
  • FirstOrder.Language.Structure.mk₂
  • FirstOrder.Language.card_mk₂
  • FirstOrder.Language.constants_mk₂
  • FirstOrder.Language.funMap_apply₀
  • FirstOrder.Language.funMap_apply₁
  • FirstOrder.Language.funMap_apply₂
  • FirstOrder.Language.funMap₂
  • FirstOrder.Language.inhabited₀
  • FirstOrder.Language.inhabited₁
  • FirstOrder.Language.inhabited₂
  • FirstOrder.Language.isAlgebraic_mk₂
  • FirstOrder.Language.isRelational_mk₂
  • FirstOrder.Language.lift_mk
  • FirstOrder.Language.mk₂_funext
  • FirstOrder.Language.relMap_apply₁
  • FirstOrder.Language.relMap_apply₂
  • FirstOrder.Language.subsingleton_mk₂_functions
  • FirstOrder.Language.subsingleton_mk₂_relations
  • FirstOrder.Language.sum_card
  • FirstOrder.Language.mk₂

Estimated changes