Documentation

Linglib.Fragments.German.Adjectives

German adjective declension #

This file defines the endings of German attributive adjectives and the principle that chooses between them. An adjective declines when it stands before its noun, and has no ending in the predicate. It has two sets of endings. The strong endings are those of dieser, but for -en in the genitive singular masculine and neuter; the weak endings are -e in the nominative singular and in the accusative singular feminine and neuter, and -en everywhere else. Durrell gives one principle that chooses between them: an adjective takes the strong endings when no determiner in its noun phrase has an ending, and the weak endings when one does. So it is strong with no determiner, weak after the definite article and dieser, and after ein, kein and the possessives strong in the three cells where they have no ending and weak in the rest. That last declension, which seems to mix the other two and is sometimes called the mixed declension, is not a third declension.

Adjectives agree with the grammatical gender of their noun, also where it is not the sex of the referent: ein junges Mädchen 'a young girl'.

Main definitions #

Main results #

References #

source
def German.Adjectives.strong (x : Determiners.GenderNumber) (c : Case) :
String

strong x c is the strong ending of the cell, the ending of dieser except for -en in the genitive singular masculine and neuter.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def German.Adjectives.weak (x : Determiners.GenderNumber) (c : Case) :
    String

    weak x c is the weak ending of the cell, -e in the nominative singular and in the accusative singular feminine and neuter and -en everywhere else.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      inductive German.Adjectives.Preceding :
      Type

      An adjective is preceded in its noun phrase by no determiner, by a determiner with an ending in every cell such as the definite article or dieser, or by an ein-word.

      Instances For
        source
        @[instance_reducible]
        instance German.Adjectives.instDecidableEqPreceding :
        DecidableEq Preceding
        Equations
        source
        def German.Adjectives.instReprPreceding.repr :
        Preceding → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[instance_reducible]
          instance German.Adjectives.instReprPreceding :
          Repr Preceding
          Equations
          source
          @[instance_reducible]
          instance German.Adjectives.instFintypePreceding :
          Fintype Preceding
          Equations
          • One or more equations did not get rendered due to their size.
          source
          def German.Adjectives.Preceding.HasEnding :
          Preceding → Determiners.GenderNumber → Case → Prop

          p.HasEnding x c holds when the preceding determiner has an ending in the cell.

          Equations
          Instances For
            source
            @[instance_reducible]
            instance German.Adjectives.instDecidableHasEnding (p : Preceding) (x : Determiners.GenderNumber) (c : Case) :
            Decidable (p.HasEnding x c)
            Equations
            source
            def German.Adjectives.ending (p : Preceding) (x : Determiners.GenderNumber) (c : Case) :
            String

            An adjective takes the weak ending when the preceding determiner has an ending, and the strong ending when there is none.

            Equations
            Instances For
              source
              @[simp]
              theorem German.Adjectives.ending_none :
              ending Preceding.none = strong

              With no determiner an adjective takes the strong endings.

              source
              @[simp]
              theorem German.Adjectives.ending_inflected :
              ending Preceding.inflected = weak

              After a determiner with an ending in every cell an adjective takes the weak endings.

              source
              theorem German.Adjectives.ending_einWord_ne_weak_iff (x : Determiners.GenderNumber) (c : Case) :
              ending Preceding.einWord x c ≠ weak x c ↔ Determiners.Endingless x c

              After an ein-word an adjective departs from the weak endings exactly in the cells where the determiner has no ending.

              source
              theorem German.Adjectives.ein_junges_maedchen :
              Determiners.ein (Determiners.GenderNumber.sg Gender.maedchen.gender) Case.nom = some "ein" ∧ "jung" ++ ending Preceding.einWord (Determiners.GenderNumber.sg Gender.maedchen.gender) Case.nom = "junges" ∧ Determiners.ein (Determiners.GenderNumber.sg Gender.Value.fem) Case.nom = some "eine" ∧ "jung" ++ ending Preceding.einWord (Determiners.GenderNumber.sg Gender.Value.fem) Case.nom = "junge"

              The noun phrase ein junges Mädchen 'a young girl' agrees with the gender the suffix fixes: Mädchen is neuter, ein has no ending in the nominative singular neuter, and the adjective takes the strong -es. The feminine, the sex of the referent, would give eine junge.