inductive Phenomena.Quantification.Data.Availability : Type

Available scope readings for a sentence

• ambiguous : Availability
• surfaceOnly : Availability
• inverseOnly : Availability

instance Phenomena.Quantification.Data.instDecidableEqAvailability : DecidableEq Availability

Equations

• Phenomena.Quantification.Data.instDecidableEqAvailability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Quantification.Data.instBEqAvailability : BEq Availability

Equations

• Phenomena.Quantification.Data.instBEqAvailability = { beq := Phenomena.Quantification.Data.instBEqAvailability.beq }

def Phenomena.Quantification.Data.instBEqAvailability.beq : Availability → Availability → Bool

Equations

• Phenomena.Quantification.Data.instBEqAvailability.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Quantification.Data.instReprAvailability.repr : Availability → Nat → Std.Format

Equations

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

instance Phenomena.Quantification.Data.instReprAvailability : Repr Availability

Equations

• Phenomena.Quantification.Data.instReprAvailability = { reprPrec := Phenomena.Quantification.Data.instReprAvailability.repr }

instance Phenomena.Quantification.Data.instInhabitedAvailability : Inhabited Availability

Equations

• Phenomena.Quantification.Data.instInhabitedAvailability = { default := Phenomena.Quantification.Data.instInhabitedAvailability.default }

def Phenomena.Quantification.Data.instInhabitedAvailability.default : Availability

Equations

• Phenomena.Quantification.Data.instInhabitedAvailability.default = Phenomena.Quantification.Data.Availability.ambiguous

inductive Phenomena.Quantification.Data.Confidence : Type

Confidence in the judgment

• clear : Confidence
• gradient : Confidence
• controversial : Confidence

instance Phenomena.Quantification.Data.instDecidableEqConfidence : DecidableEq Confidence

Equations

• Phenomena.Quantification.Data.instDecidableEqConfidence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Data.instBEqConfidence.beq : Confidence → Confidence → Bool

Equations

• Phenomena.Quantification.Data.instBEqConfidence.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Quantification.Data.instBEqConfidence : BEq Confidence

Equations

• Phenomena.Quantification.Data.instBEqConfidence = { beq := Phenomena.Quantification.Data.instBEqConfidence.beq }

def Phenomena.Quantification.Data.instReprConfidence.repr : Confidence → Nat → Std.Format

Equations

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

instance Phenomena.Quantification.Data.instReprConfidence : Repr Confidence

Equations

• Phenomena.Quantification.Data.instReprConfidence = { reprPrec := Phenomena.Quantification.Data.instReprConfidence.repr }

def Phenomena.Quantification.Data.instInhabitedConfidence.default : Confidence

Equations

• Phenomena.Quantification.Data.instInhabitedConfidence.default = Phenomena.Quantification.Data.Confidence.clear

instance Phenomena.Quantification.Data.instInhabitedConfidence : Inhabited Confidence

Equations

• Phenomena.Quantification.Data.instInhabitedConfidence = { default := Phenomena.Quantification.Data.instInhabitedConfidence.default }

inductive Phenomena.Quantification.Data.DataSource : Type

Source of the judgment

• introspective : DataSource
• experimental : DataSource
• corpus : DataSource

instance Phenomena.Quantification.Data.instDecidableEqDataSource : DecidableEq DataSource

Equations

• Phenomena.Quantification.Data.instDecidableEqDataSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Data.instBEqDataSource.beq : DataSource → DataSource → Bool

Equations

• Phenomena.Quantification.Data.instBEqDataSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Quantification.Data.instBEqDataSource : BEq DataSource

Equations

• Phenomena.Quantification.Data.instBEqDataSource = { beq := Phenomena.Quantification.Data.instBEqDataSource.beq }

def Phenomena.Quantification.Data.instReprDataSource.repr : DataSource → Nat → Std.Format

Equations

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

instance Phenomena.Quantification.Data.instReprDataSource : Repr DataSource

Equations

• Phenomena.Quantification.Data.instReprDataSource = { reprPrec := Phenomena.Quantification.Data.instReprDataSource.repr }

def Phenomena.Quantification.Data.instInhabitedDataSource.default : DataSource

Equations

• Phenomena.Quantification.Data.instInhabitedDataSource.default = Phenomena.Quantification.Data.DataSource.introspective

instance Phenomena.Quantification.Data.instInhabitedDataSource : Inhabited DataSource

Equations

• Phenomena.Quantification.Data.instInhabitedDataSource = { default := Phenomena.Quantification.Data.instInhabitedDataSource.default }

inductive Phenomena.Quantification.Data.FreezingContext : Type

Types of configurations that induce scope freezing

• none : FreezingContext
• possessor : FreezingContext
• doubleObject : FreezingContext
• passive : FreezingContext
• heavyNP : FreezingContext
• weakCrossover : FreezingContext
• adjunct : FreezingContext
• attitude : FreezingContext

instance Phenomena.Quantification.Data.instDecidableEqFreezingContext : DecidableEq FreezingContext

Equations

• Phenomena.Quantification.Data.instDecidableEqFreezingContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Quantification.Data.instBEqFreezingContext : BEq FreezingContext

Equations

• Phenomena.Quantification.Data.instBEqFreezingContext = { beq := Phenomena.Quantification.Data.instBEqFreezingContext.beq }

def Phenomena.Quantification.Data.instBEqFreezingContext.beq : FreezingContext → FreezingContext → Bool

Equations

• Phenomena.Quantification.Data.instBEqFreezingContext.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Quantification.Data.instReprFreezingContext.repr : FreezingContext → Nat → Std.Format

Equations

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

instance Phenomena.Quantification.Data.instReprFreezingContext : Repr FreezingContext

Equations

• Phenomena.Quantification.Data.instReprFreezingContext = { reprPrec := Phenomena.Quantification.Data.instReprFreezingContext.repr }

def Phenomena.Quantification.Data.instInhabitedFreezingContext.default : FreezingContext

Equations

• Phenomena.Quantification.Data.instInhabitedFreezingContext.default = Phenomena.Quantification.Data.FreezingContext.none

instance Phenomena.Quantification.Data.instInhabitedFreezingContext : Inhabited FreezingContext

Equations

• Phenomena.Quantification.Data.instInhabitedFreezingContext = { default := Phenomena.Quantification.Data.instInhabitedFreezingContext.default }

structure Phenomena.Quantification.Data.Example : Type

A scope freezing example with empirical judgment

• id : String
• sentence : String
• quant1 : String
• quant2 : String
• context : FreezingContext
• observed : Availability
• confidence : Confidence
• source : DataSource
• surfaceGloss : String
• inverseGloss : String
• notes : String

def Phenomena.Quantification.Data.instReprExample.repr : Example → Nat → Std.Format

Equations

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

instance Phenomena.Quantification.Data.instReprExample : Repr Example

Equations

• Phenomena.Quantification.Data.instReprExample = { reprPrec := Phenomena.Quantification.Data.instReprExample.repr }

def Phenomena.Quantification.Data.possessor_baseline : Example

Equations

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

def Phenomena.Quantification.Data.possessor_frozen : Example

Equations

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

def Phenomena.Quantification.Data.possessor_variant1 : Example

Equations

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

def Phenomena.Quantification.Data.possessor_variant2 : Example

Equations

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

def Phenomena.Quantification.Data.dative_baseline : Example

Equations

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

def Phenomena.Quantification.Data.dative_frozen : Example

Equations

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

def Phenomena.Quantification.Data.dative_variant : Example

Equations

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

def Phenomena.Quantification.Data.passive_baseline : Example

Equations

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

def Phenomena.Quantification.Data.passive_frozen : Example

Equations

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

def Phenomena.Quantification.Data.passive_variant : Example

Equations

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

def Phenomena.Quantification.Data.heavy_baseline : Example

Equations

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

def Phenomena.Quantification.Data.heavy_frozen : Example

Equations

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

def Phenomena.Quantification.Data.crossover_baseline : Example

Equations

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

def Phenomena.Quantification.Data.crossover_frozen : Example

Equations

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

def Phenomena.Quantification.Data.attitude_frozen : Example

Equations

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

def Phenomena.Quantification.Data.possessorExamples : List Example

Equations

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

def Phenomena.Quantification.Data.doubleObjectExamples : List Example

Equations

• Phenomena.Quantification.Data.doubleObjectExamples = [Phenomena.Quantification.Data.dative_baseline, Phenomena.Quantification.Data.dative_frozen, Phenomena.Quantification.Data.dative_variant]

def Phenomena.Quantification.Data.passiveExamples : List Example

Equations

• Phenomena.Quantification.Data.passiveExamples = [Phenomena.Quantification.Data.passive_baseline, Phenomena.Quantification.Data.passive_frozen, Phenomena.Quantification.Data.passive_variant]

def Phenomena.Quantification.Data.heavyNPExamples : List Example

Equations

• Phenomena.Quantification.Data.heavyNPExamples = [Phenomena.Quantification.Data.heavy_baseline, Phenomena.Quantification.Data.heavy_frozen]

def Phenomena.Quantification.Data.crossoverExamples : List Example

Equations

• Phenomena.Quantification.Data.crossoverExamples = [Phenomena.Quantification.Data.crossover_baseline, Phenomena.Quantification.Data.crossover_frozen]

def Phenomena.Quantification.Data.attitudeExamples : List Example

Equations

• Phenomena.Quantification.Data.attitudeExamples = [Phenomena.Quantification.Data.attitude_frozen]

def Phenomena.Quantification.Data.allExamples : List Example

Equations

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

def Phenomena.Quantification.Data.possessorFreezingIsClear : Bool

Possessor freezing is robust (clear judgments)

Equations

• Phenomena.Quantification.Data.possessorFreezingIsClear = (Phenomena.Quantification.Data.possessor_frozen.confidence == Phenomena.Quantification.Data.Confidence.clear)

def Phenomena.Quantification.Data.doubleObjectFreezingIsClear : Bool

Double object freezing is robust

Equations

• Phenomena.Quantification.Data.doubleObjectFreezingIsClear = (Phenomena.Quantification.Data.dative_frozen.confidence == Phenomena.Quantification.Data.Confidence.clear)

def Phenomena.Quantification.Data.passiveFreezingIsGradient : Bool

Passive freezing is more gradient

Equations

• Phenomena.Quantification.Data.passiveFreezingIsGradient = (Phenomena.Quantification.Data.passive_frozen.confidence == Phenomena.Quantification.Data.Confidence.gradient)

def Phenomena.Quantification.Data.frozenCount : Nat

Count frozen examples

Equations

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

def Phenomena.Quantification.Data.ambiguousCount : Nat

Count ambiguous baselines

Equations

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

inductive Phenomena.Quantification.Data.RoundnessLevel : Type

Roundness level of a numeral.

• exact : RoundnessLevel
• round1 : RoundnessLevel
• round2 : RoundnessLevel
• round3 : RoundnessLevel

def Phenomena.Quantification.Data.instReprRoundnessLevel.repr : RoundnessLevel → Nat → Std.Format

Equations

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

instance Phenomena.Quantification.Data.instReprRoundnessLevel : Repr RoundnessLevel

Equations

• Phenomena.Quantification.Data.instReprRoundnessLevel = { reprPrec := Phenomena.Quantification.Data.instReprRoundnessLevel.repr }

instance Phenomena.Quantification.Data.instDecidableEqRoundnessLevel : DecidableEq RoundnessLevel

Equations

• Phenomena.Quantification.Data.instDecidableEqRoundnessLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Quantification.Data.classifyRoundness (n : Nat) : RoundnessLevel

Classify numeral roundness.

Equations

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

structure Phenomena.Quantification.Data.NumeralImprecisionDatum : Type

Numeral imprecision datum: context-dependent exactness.

• numeral : Nat
• roundness : RoundnessLevel
• sentenceFrame : String
• exactContext : String
• inexactContext : String
• actualValue : Nat
• acceptableExact : Bool
• acceptableInexact : Bool

def Phenomena.Quantification.Data.instReprNumeralImprecisionDatum.repr : NumeralImprecisionDatum → Nat → Std.Format

Equations

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

instance Phenomena.Quantification.Data.instReprNumeralImprecisionDatum : Repr NumeralImprecisionDatum

Equations

• Phenomena.Quantification.Data.instReprNumeralImprecisionDatum = { reprPrec := Phenomena.Quantification.Data.instReprNumeralImprecisionDatum.repr }

def Phenomena.Quantification.Data.carsExact : NumeralImprecisionDatum

The cars scenario.

Equations

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

def Phenomena.Quantification.Data.carsNonRound : NumeralImprecisionDatum

Equations

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

structure Phenomena.Quantification.Data.RoundnessAsymmetryDatum : Type

Minimal pair showing round/non-round asymmetry.

• roundNumeral : Nat
• nonRoundNumeral : Nat
• context : String
• actualValue : Nat
• roundAcceptable : Bool
• nonRoundAcceptable : Bool

instance Phenomena.Quantification.Data.instReprRoundnessAsymmetryDatum : Repr RoundnessAsymmetryDatum

Equations

• Phenomena.Quantification.Data.instReprRoundnessAsymmetryDatum = { reprPrec := Phenomena.Quantification.Data.instReprRoundnessAsymmetryDatum.repr }

def Phenomena.Quantification.Data.instReprRoundnessAsymmetryDatum.repr : RoundnessAsymmetryDatum → Nat → Std.Format

Equations

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

def Phenomena.Quantification.Data.hundredVsNinetyNine : RoundnessAsymmetryDatum

Equations

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

def Phenomena.Quantification.Data.fiftyVsFortyNine : RoundnessAsymmetryDatum

Equations

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

structure Phenomena.Quantification.Data.NegationConstraintDatum : Type

Numerals under negation require polar questions.

• positiveSentence : String
• negativeSentence : String
• howManyContext : String
• polarContext : String
• negativeOkHowMany : Bool
• negativeOkPolar : Bool

instance Phenomena.Quantification.Data.instReprNegationConstraintDatum : Repr NegationConstraintDatum

Equations

• Phenomena.Quantification.Data.instReprNegationConstraintDatum = { reprPrec := Phenomena.Quantification.Data.instReprNegationConstraintDatum.repr }

def Phenomena.Quantification.Data.instReprNegationConstraintDatum.repr : NegationConstraintDatum → Nat → Std.Format

Equations

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

def Phenomena.Quantification.Data.sheepNegation : NegationConstraintDatum

Equations

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

structure Phenomena.Quantification.Data.GameShowDatum : Type

Game show scenario testing for homogeneity gaps.

• sentence : String
• scenario : String
• exactReadingTrue : Bool
• inexactReadingTrue : Bool
• acceptable : Bool
• speakersAgree : Bool
• notes : String

instance Phenomena.Quantification.Data.instReprGameShowDatum : Repr GameShowDatum

Equations

• Phenomena.Quantification.Data.instReprGameShowDatum = { reprPrec := Phenomena.Quantification.Data.instReprGameShowDatum.repr }

def Phenomena.Quantification.Data.instReprGameShowDatum.repr : GameShowDatum → Nat → Std.Format

Equations

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

def Phenomena.Quantification.Data.gameShowPositive : GameShowDatum

Equations

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

def Phenomena.Quantification.Data.gameShowNegative : GameShowDatum

Equations

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

structure Phenomena.Quantification.Data.ExactlyModifierDatum : Type

"Exactly" removes imprecision.

• bareSentence : String
• exactlySentence : String
• context : String
• actualValue : Nat
• bareAcceptable : Bool
• exactlyAcceptable : Bool

instance Phenomena.Quantification.Data.instReprExactlyModifierDatum : Repr ExactlyModifierDatum

Equations

• Phenomena.Quantification.Data.instReprExactlyModifierDatum = { reprPrec := Phenomena.Quantification.Data.instReprExactlyModifierDatum.repr }

def Phenomena.Quantification.Data.instReprExactlyModifierDatum.repr : ExactlyModifierDatum → Nat → Std.Format

Equations

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

def Phenomena.Quantification.Data.exactlyRemovesImprecision : ExactlyModifierDatum

Equations

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

structure Phenomena.Quantification.Data.ApproximatelyDatum : Type

"Approximately" makes imprecision explicit.

• bareSentence : String
• approxSentence : String
• roundness : RoundnessLevel
• approxNatural : Bool
• notes : String

def Phenomena.Quantification.Data.instReprApproximatelyDatum.repr : ApproximatelyDatum → Nat → Std.Format

Equations

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

instance Phenomena.Quantification.Data.instReprApproximatelyDatum : Repr ApproximatelyDatum

Equations

• Phenomena.Quantification.Data.instReprApproximatelyDatum = { reprPrec := Phenomena.Quantification.Data.instReprApproximatelyDatum.repr }

def Phenomena.Quantification.Data.approximatelyWithRound : ApproximatelyDatum

Equations

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

def Phenomena.Quantification.Data.approximatelyWithNonRound : ApproximatelyDatum

Equations

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

structure Phenomena.Quantification.Data.TimeExpressionDatum : Type

Time expressions show round/non-round patterns.

• sentence : String
• timeExpression : String
• round : Bool
• scenario : String
• actualTime : String
• acceptable : Bool

def Phenomena.Quantification.Data.instReprTimeExpressionDatum.repr : TimeExpressionDatum → Nat → Std.Format

Equations

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

instance Phenomena.Quantification.Data.instReprTimeExpressionDatum : Repr TimeExpressionDatum

Equations

• Phenomena.Quantification.Data.instReprTimeExpressionDatum = { reprPrec := Phenomena.Quantification.Data.instReprTimeExpressionDatum.repr }

def Phenomena.Quantification.Data.arriveAt3 : TimeExpressionDatum

Equations

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

def Phenomena.Quantification.Data.arriveAt258 : TimeExpressionDatum

Equations

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

structure Phenomena.Quantification.Data.GranularityDatum : Type

Granularity affects which numerals count as "round."

• numeral : Nat
• coarseScale : String
• roundOnCoarse : Bool
• fineScale : String
• roundOnFine : Bool

def Phenomena.Quantification.Data.instReprGranularityDatum.repr : GranularityDatum → Nat → Std.Format

Equations

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

instance Phenomena.Quantification.Data.instReprGranularityDatum : Repr GranularityDatum

Equations

• Phenomena.Quantification.Data.instReprGranularityDatum = { reprPrec := Phenomena.Quantification.Data.instReprGranularityDatum.repr }

def Phenomena.Quantification.Data.granularityExample : GranularityDatum

Equations

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

structure Phenomena.Quantification.Data.NumeralImprecisionGeneralizations : Type

Core empirical generalizations about numeral imprecision.

• roundPermitsImprecision : Bool
• nonRoundRequiresExact : Bool
• exactlyRemoves : Bool
• negationRequiresPolar : Bool
• noHomogeneityGaps : Bool
• contextSensitive : Bool

def Phenomena.Quantification.Data.instReprNumeralImprecisionGeneralizations.repr : NumeralImprecisionGeneralizations → Nat → Std.Format

Equations

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

instance Phenomena.Quantification.Data.instReprNumeralImprecisionGeneralizations : Repr NumeralImprecisionGeneralizations

Equations

• Phenomena.Quantification.Data.instReprNumeralImprecisionGeneralizations = { reprPrec := Phenomena.Quantification.Data.instReprNumeralImprecisionGeneralizations.repr }

def Phenomena.Quantification.Data.mainGeneralizations : NumeralImprecisionGeneralizations

Equations

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

def Phenomena.Quantification.Data.carsExamples : List NumeralImprecisionDatum

Equations

• Phenomena.Quantification.Data.carsExamples = [Phenomena.Quantification.Data.carsExact, Phenomena.Quantification.Data.carsNonRound]

def Phenomena.Quantification.Data.roundnessAsymmetryExamples : List RoundnessAsymmetryDatum

Equations

• Phenomena.Quantification.Data.roundnessAsymmetryExamples = [Phenomena.Quantification.Data.hundredVsNinetyNine, Phenomena.Quantification.Data.fiftyVsFortyNine]

def Phenomena.Quantification.Data.gameShowExamples : List GameShowDatum

Equations

• Phenomena.Quantification.Data.gameShowExamples = [Phenomena.Quantification.Data.gameShowPositive, Phenomena.Quantification.Data.gameShowNegative]

inductive Phenomena.Quantification.Data.VerbOrder : Type

Word order patterns in verb-final constructions.

• verbRaising : VerbOrder
• verbProjectionRaising : VerbOrder

instance Phenomena.Quantification.Data.instDecidableEqVerbOrder : DecidableEq VerbOrder

Equations

• Phenomena.Quantification.Data.instDecidableEqVerbOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Quantification.Data.instBEqVerbOrder : BEq VerbOrder

Equations

• Phenomena.Quantification.Data.instBEqVerbOrder = { beq := Phenomena.Quantification.Data.instBEqVerbOrder.beq }

def Phenomena.Quantification.Data.instBEqVerbOrder.beq : VerbOrder → VerbOrder → Bool

Equations

• Phenomena.Quantification.Data.instBEqVerbOrder.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Quantification.Data.instReprVerbOrder.repr : VerbOrder → Nat → Std.Format

Equations

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

instance Phenomena.Quantification.Data.instReprVerbOrder : Repr VerbOrder

Equations

• Phenomena.Quantification.Data.instReprVerbOrder = { reprPrec := Phenomena.Quantification.Data.instReprVerbOrder.repr }

def Phenomena.Quantification.Data.instInhabitedVerbOrder.default : VerbOrder

Equations

• Phenomena.Quantification.Data.instInhabitedVerbOrder.default = Phenomena.Quantification.Data.VerbOrder.verbRaising

instance Phenomena.Quantification.Data.instInhabitedVerbOrder : Inhabited VerbOrder

Equations

• Phenomena.Quantification.Data.instInhabitedVerbOrder = { default := Phenomena.Quantification.Data.instInhabitedVerbOrder.default }

def Phenomena.Quantification.Data.blocksInverseScope : VerbOrder → Bool

Whether a word order blocks inverse scope

Equations

• Phenomena.Quantification.Data.blocksInverseScope Phenomena.Quantification.Data.VerbOrder.verbRaising = false
• Phenomena.Quantification.Data.blocksInverseScope Phenomena.Quantification.Data.VerbOrder.verbProjectionRaising = true

inductive Phenomena.Quantification.Data.ScopeAvailability : Type

Available scope readings for a sentence.

• surfaceOnly : ScopeAvailability
• ambiguous : ScopeAvailability

instance Phenomena.Quantification.Data.instDecidableEqScopeAvailability : DecidableEq ScopeAvailability

Equations

• Phenomena.Quantification.Data.instDecidableEqScopeAvailability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Quantification.Data.instBEqScopeAvailability : BEq ScopeAvailability

Equations

• Phenomena.Quantification.Data.instBEqScopeAvailability = { beq := Phenomena.Quantification.Data.instBEqScopeAvailability.beq }

def Phenomena.Quantification.Data.instBEqScopeAvailability.beq : ScopeAvailability → ScopeAvailability → Bool

Equations

• Phenomena.Quantification.Data.instBEqScopeAvailability.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Quantification.Data.instReprScopeAvailability.repr : ScopeAvailability → Nat → Std.Format

Equations

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

instance Phenomena.Quantification.Data.instReprScopeAvailability : Repr ScopeAvailability

Equations

• Phenomena.Quantification.Data.instReprScopeAvailability = { reprPrec := Phenomena.Quantification.Data.instReprScopeAvailability.repr }

def Phenomena.Quantification.Data.instInhabitedScopeAvailability.default : ScopeAvailability

Equations

• Phenomena.Quantification.Data.instInhabitedScopeAvailability.default = Phenomena.Quantification.Data.ScopeAvailability.surfaceOnly

instance Phenomena.Quantification.Data.instInhabitedScopeAvailability : Inhabited ScopeAvailability

Equations

• Phenomena.Quantification.Data.instInhabitedScopeAvailability = { default := Phenomena.Quantification.Data.instInhabitedScopeAvailability.default }

def Phenomena.Quantification.Data.wordOrderToAvailability : VerbOrder → ScopeAvailability

Convert word order to scope availability

Equations

• Phenomena.Quantification.Data.wordOrderToAvailability Phenomena.Quantification.Data.VerbOrder.verbRaising = Phenomena.Quantification.Data.ScopeAvailability.ambiguous
• Phenomena.Quantification.Data.wordOrderToAvailability Phenomena.Quantification.Data.VerbOrder.verbProjectionRaising = Phenomena.Quantification.Data.ScopeAvailability.surfaceOnly

structure Phenomena.Quantification.Data.GermanScopeExample : Type

German sentence data from Bayer/Kayne.

• surface : String
• translation : String
• wordOrder : VerbOrder
• observed : ScopeAvailability

instance Phenomena.Quantification.Data.instReprGermanScopeExample : Repr GermanScopeExample

Equations

• Phenomena.Quantification.Data.instReprGermanScopeExample = { reprPrec := Phenomena.Quantification.Data.instReprGermanScopeExample.repr }

def Phenomena.Quantification.Data.instReprGermanScopeExample.repr : GermanScopeExample → Nat → Std.Format

Equations

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

def Phenomena.Quantification.Data.german_96 : GermanScopeExample

Equations

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

def Phenomena.Quantification.Data.german_97 : GermanScopeExample

Equations

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

structure Phenomena.Quantification.Data.WestFlemishScopeExample : Type

West Flemish data from @cite{haegeman-van-riemsdijk-1986}.

• surface : String
• translation : String
• wordOrder : VerbOrder
• observed : ScopeAvailability

def Phenomena.Quantification.Data.instReprWestFlemishScopeExample.repr : WestFlemishScopeExample → Nat → Std.Format

Equations

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

instance Phenomena.Quantification.Data.instReprWestFlemishScopeExample : Repr WestFlemishScopeExample

Equations

• Phenomena.Quantification.Data.instReprWestFlemishScopeExample = { reprPrec := Phenomena.Quantification.Data.instReprWestFlemishScopeExample.repr }

def Phenomena.Quantification.Data.westFlemish_98a : WestFlemishScopeExample

Equations

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

def Phenomena.Quantification.Data.westFlemish_98b : WestFlemishScopeExample

Equations

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

structure Phenomena.Quantification.Data.DutchScopeExample : Type

Dutch equi verb data from @cite{steedman-2000}.

• surface : String
• translation : String
• wordOrder : VerbOrder
• observed : ScopeAvailability
• quantifiers : List String

instance Phenomena.Quantification.Data.instReprDutchScopeExample : Repr DutchScopeExample

Equations

• Phenomena.Quantification.Data.instReprDutchScopeExample = { reprPrec := Phenomena.Quantification.Data.instReprDutchScopeExample.repr }

def Phenomena.Quantification.Data.instReprDutchScopeExample.repr : DutchScopeExample → Nat → Std.Format

Equations

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

def Phenomena.Quantification.Data.dutch_99a : DutchScopeExample

Equations

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

def Phenomena.Quantification.Data.dutch_99b : DutchScopeExample

Equations

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

def Phenomena.Quantification.Data.dutch_100a : DutchScopeExample

Equations

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

def Phenomena.Quantification.Data.dutch_100b : DutchScopeExample

Equations

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

def Phenomena.Quantification.Data.allDutchExamples : List DutchScopeExample

Equations

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

def Phenomena.Quantification.Data.allWestFlemishExamples : List WestFlemishScopeExample

Equations

• Phenomena.Quantification.Data.allWestFlemishExamples = [Phenomena.Quantification.Data.westFlemish_98a, Phenomena.Quantification.Data.westFlemish_98b]

def Phenomena.Quantification.Data.allGermanExamples : List GermanScopeExample

Equations

• Phenomena.Quantification.Data.allGermanExamples = [Phenomena.Quantification.Data.german_96, Phenomena.Quantification.Data.german_97]

theorem Phenomena.Quantification.Data.wordOrder_predicts_dutch_99a : wordOrderToAvailability dutch_99a.wordOrder = dutch_99a.observed

Word order correctly predicts scope availability

theorem Phenomena.Quantification.Data.wordOrder_predicts_dutch_99b : wordOrderToAvailability dutch_99b.wordOrder = dutch_99b.observed

theorem Phenomena.Quantification.Data.wordOrder_predicts_dutch_100a : wordOrderToAvailability dutch_100a.wordOrder = dutch_100a.observed

theorem Phenomena.Quantification.Data.wordOrder_predicts_dutch_100b : wordOrderToAvailability dutch_100b.wordOrder = dutch_100b.observed

theorem Phenomena.Quantification.Data.wordOrder_predicts_german_96 : wordOrderToAvailability german_96.wordOrder = german_96.observed

theorem Phenomena.Quantification.Data.wordOrder_predicts_german_97 : wordOrderToAvailability german_97.wordOrder = german_97.observed