inductive Phenomena.Plurals.Studies.HaslingerEtAl2025.SyntacticUse : Type

Syntactic distribution of a distributive element

• dpInternal : SyntacticUse
• distance : SyntacticUse

instance Phenomena.Plurals.Studies.HaslingerEtAl2025.instDecidableEqSyntacticUse : DecidableEq SyntacticUse

Equations

• Phenomena.Plurals.Studies.HaslingerEtAl2025.instDecidableEqSyntacticUse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprSyntacticUse : Repr SyntacticUse

Equations

• Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprSyntacticUse = { reprPrec := Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprSyntacticUse.repr }

def Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprSyntacticUse.repr : SyntacticUse → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Plurals.Studies.HaslingerEtAl2025.instBEqSyntacticUse.beq : SyntacticUse → SyntacticUse → Bool

Equations

• Phenomena.Plurals.Studies.HaslingerEtAl2025.instBEqSyntacticUse.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Plurals.Studies.HaslingerEtAl2025.instBEqSyntacticUse : BEq SyntacticUse

Equations

• Phenomena.Plurals.Studies.HaslingerEtAl2025.instBEqSyntacticUse = { beq := Phenomena.Plurals.Studies.HaslingerEtAl2025.instBEqSyntacticUse.beq }

structure Phenomena.Plurals.Studies.HaslingerEtAl2025.LexicalItem : Type

A German distributive item with its properties

• form : String
• gloss : String
• uses : List SyntacticUse
• semanticClass : Semantics.Lexical.Plural.Distributivity.DistMaxClass

instance Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprLexicalItem : Repr LexicalItem

Equations

• Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprLexicalItem = { reprPrec := Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprLexicalItem.repr }

def Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprLexicalItem.repr : LexicalItem → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Plurals.Studies.HaslingerEtAl2025.jeder : LexicalItem

jeder (DP-internal and distance): +distributive, +maximal

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Plurals.Studies.HaslingerEtAl2025.jeweils : LexicalItem

jeweils (distance only): +distributive, -maximal

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Plurals.Studies.HaslingerEtAl2025.alle : LexicalItem

alle (DP-internal): -distributive, +maximal

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Plurals.Studies.HaslingerEtAl2025.definitePlural : LexicalItem

Definite plurals: -distributive, -maximal

Equations

• One or more equations did not get rendered due to their size.

structure Phenomena.Plurals.Studies.HaslingerEtAl2025.NonMaxContext : Type

Context for testing non-maximality (QUD makes exceptions irrelevant)

• description : String
• totalItems : ℕ
• exceptions : ℕ
• implicitQUD : String

instance Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprNonMaxContext : Repr NonMaxContext

Equations

• Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprNonMaxContext = { reprPrec := Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprNonMaxContext.repr }

def Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprNonMaxContext.repr : NonMaxContext → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Plurals.Studies.HaslingerEtAl2025.magnetsContext : NonMaxContext

Magnets scenario (example 23): 5 boxes, 4 have 2 magnets, 1 has 1

Equations

• One or more equations did not get rendered due to their size.

structure Phenomena.Plurals.Studies.HaslingerEtAl2025.Observation : Type

Experimental observation

• item : LexicalItem
• context : NonMaxContext
• acceptanceRate : Float

  Proportion accepting (rating ≥ 4 on 7-point scale)

def Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprObservation.repr : Observation → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprObservation : Repr Observation

Equations

• Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprObservation = { reprPrec := Phenomena.Plurals.Studies.HaslingerEtAl2025.instReprObservation.repr }

def Phenomena.Plurals.Studies.HaslingerEtAl2025.jederInNonMax : Observation

jeder rejected in non-maximal contexts (Figure 1)

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Plurals.Studies.HaslingerEtAl2025.jeweilsInNonMax : Observation

jeweils shows mixed judgments (Figure 1)

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Plurals.Studies.HaslingerEtAl2025.isDistributive : Semantics.Lexical.Plural.Distributivity.DistMaxClass → Bool

Both jeder and jeweils are distributive

Equations

• Phenomena.Plurals.Studies.HaslingerEtAl2025.isDistributive Semantics.Lexical.Plural.Distributivity.DistMaxClass.distMax = true
• Phenomena.Plurals.Studies.HaslingerEtAl2025.isDistributive Semantics.Lexical.Plural.Distributivity.DistMaxClass.distNonMax = true
• Phenomena.Plurals.Studies.HaslingerEtAl2025.isDistributive Semantics.Lexical.Plural.Distributivity.DistMaxClass.nonDistMax = false
• Phenomena.Plurals.Studies.HaslingerEtAl2025.isDistributive Semantics.Lexical.Plural.Distributivity.DistMaxClass.nonDistNonMax = false

theorem Phenomena.Plurals.Studies.HaslingerEtAl2025.independence_attested : isDistributive jeder.semanticClass = isDistributive jeweils.semanticClass ∧ jeder.semanticClass ≠ jeweils.semanticClass

The independence claim: same distributivity, different maximality

def Phenomena.Plurals.Studies.HaslingerEtAl2025.hasDPUse (item : LexicalItem) : Bool

Correlation (Section 4): No DP use ↔ permits non-maximality?

Equations

• Phenomena.Plurals.Studies.HaslingerEtAl2025.hasDPUse item = item.uses.contains Phenomena.Plurals.Studies.HaslingerEtAl2025.SyntacticUse.dpInternal

def Phenomena.Plurals.Studies.HaslingerEtAl2025.typologyTable : List (String × Bool × Bool)

The typological table (5) from the paper

Equations

• One or more equations did not get rendered due to their size.