Word order samples: schema

Typed schema for the language samples of the basic order typology: a paper's classification of each language of its sample by dominant clause order, adposition type, and the orders of a noun with its genitive, adjective, demonstrative, and numeral, together with the further properties the paper records per language, and its table of order types with the languages attesting each. Generated rows live in Data/WordOrder/<Paper>.lean, emitted from the canonical <Paper>.json by scripts/gen_word_order.py.

This is data: it imports nothing from Linglib/ and states no theorems. A property is none for a language when the paper records no value for it: the language lacks the element, the paper excludes it, or the paper has no data.

References

• [Gre63]

inductive Data.WordOrder.VerbPosition : Type

The dominant order of verb, nominal subject, and nominal object, by the verb's position, for verb-subject-object, subject-verb-object, and subject-object-verb.

• initial : VerbPosition
• medial : VerbPosition
• final : VerbPosition

@[instance_reducible]

instance Data.WordOrder.instDecidableEqVerbPosition : DecidableEq VerbPosition

Equations

• Data.WordOrder.instDecidableEqVerbPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Data.WordOrder.instReprVerbPosition.repr : VerbPosition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.WordOrder.instReprVerbPosition : Repr VerbPosition

Equations

• Data.WordOrder.instReprVerbPosition = { reprPrec := Data.WordOrder.instReprVerbPosition.repr }

@[instance_reducible]

instance Data.WordOrder.instFintypeVerbPosition : Fintype VerbPosition

Equations

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

inductive Data.WordOrder.Adposition : Type

Prepositions or postpositions.

• prepositions : Adposition
• postpositions : Adposition

@[instance_reducible]

instance Data.WordOrder.instDecidableEqAdposition : DecidableEq Adposition

Equations

• Data.WordOrder.instDecidableEqAdposition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Data.WordOrder.instReprAdposition.repr : Adposition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.WordOrder.instReprAdposition : Repr Adposition

Equations

• Data.WordOrder.instReprAdposition = { reprPrec := Data.WordOrder.instReprAdposition.repr }

@[instance_reducible]

instance Data.WordOrder.instFintypeAdposition : Fintype Adposition

Equations

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

inductive Data.WordOrder.NounOrder : Type

The order of a noun and one of its dependents, the noun first, the dependent first, or both orders found.

• nounFirst : NounOrder
• dependentFirst : NounOrder
• both : NounOrder

@[instance_reducible]

instance Data.WordOrder.instDecidableEqNounOrder : DecidableEq NounOrder

Equations

• Data.WordOrder.instDecidableEqNounOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Data.WordOrder.instReprNounOrder : Repr NounOrder

Equations

• Data.WordOrder.instReprNounOrder = { reprPrec := Data.WordOrder.instReprNounOrder.repr }

def Data.WordOrder.instReprNounOrder.repr : NounOrder → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.WordOrder.instFintypeNounOrder : Fintype NounOrder

Equations

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

inductive Data.WordOrder.SentencePlace : Type

The place of an element fixed by reference to the sentence as a whole.

• initial : SentencePlace
• final : SentencePlace

@[instance_reducible]

instance Data.WordOrder.instDecidableEqSentencePlace : DecidableEq SentencePlace

Equations

• Data.WordOrder.instDecidableEqSentencePlace x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Data.WordOrder.instReprSentencePlace : Repr SentencePlace

Equations

• Data.WordOrder.instReprSentencePlace = { reprPrec := Data.WordOrder.instReprSentencePlace.repr }

def Data.WordOrder.instReprSentencePlace.repr : SentencePlace → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.WordOrder.instFintypeSentencePlace : Fintype SentencePlace

Equations

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

inductive Data.WordOrder.Placement : Type

The place of an element fixed by reference to a particular word.

• precedes : Placement
• follows : Placement

@[instance_reducible]

instance Data.WordOrder.instDecidableEqPlacement : DecidableEq Placement

Equations

• Data.WordOrder.instDecidableEqPlacement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Data.WordOrder.instReprPlacement.repr : Placement → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.WordOrder.instReprPlacement : Repr Placement

Equations

• Data.WordOrder.instReprPlacement = { reprPrec := Data.WordOrder.instReprPlacement.repr }

@[instance_reducible]

instance Data.WordOrder.instFintypePlacement : Fintype Placement

Equations

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

inductive Data.WordOrder.AdverbOrder : Type

The order of an adverb and the adjective it modifies.

• adverbAdjective : AdverbOrder
• adjectiveAdverb : AdverbOrder
• both : AdverbOrder

@[instance_reducible]

instance Data.WordOrder.instDecidableEqAdverbOrder : DecidableEq AdverbOrder

Equations

• Data.WordOrder.instDecidableEqAdverbOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Data.WordOrder.instReprAdverbOrder : Repr AdverbOrder

Equations

• Data.WordOrder.instReprAdverbOrder = { reprPrec := Data.WordOrder.instReprAdverbOrder.repr }

def Data.WordOrder.instReprAdverbOrder.repr : AdverbOrder → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.WordOrder.instFintypeAdverbOrder : Fintype AdverbOrder

Equations

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

inductive Data.WordOrder.ComparisonOrder : Type

The order of adjective, marker, and standard in a comparison of superiority.

• adjectiveMarkerStandard : ComparisonOrder
• standardMarkerAdjective : ComparisonOrder
• both : ComparisonOrder

@[instance_reducible]

instance Data.WordOrder.instDecidableEqComparisonOrder : DecidableEq ComparisonOrder

Equations

• Data.WordOrder.instDecidableEqComparisonOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Data.WordOrder.instReprComparisonOrder : Repr ComparisonOrder

Equations

• Data.WordOrder.instReprComparisonOrder = { reprPrec := Data.WordOrder.instReprComparisonOrder.repr }

def Data.WordOrder.instReprComparisonOrder.repr : ComparisonOrder → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.WordOrder.instFintypeComparisonOrder : Fintype ComparisonOrder

Equations

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

inductive Data.WordOrder.Apposition : Type

The order of a common noun and a proper noun in apposition.

• commonProper : Apposition
• properCommon : Apposition

@[instance_reducible]

instance Data.WordOrder.instDecidableEqApposition : DecidableEq Apposition

Equations

• Data.WordOrder.instDecidableEqApposition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Data.WordOrder.instReprApposition.repr : Apposition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.WordOrder.instReprApposition : Repr Apposition

Equations

• Data.WordOrder.instReprApposition = { reprPrec := Data.WordOrder.instReprApposition.repr }

@[instance_reducible]

instance Data.WordOrder.instFintypeApposition : Fintype Apposition

Equations

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

inductive Data.WordOrder.Affixing : Type

Whether a language's affixes are all suffixes, all prefixes, or of both kinds.

• suffixingOnly : Affixing
• prefixingOnly : Affixing
• both : Affixing

@[instance_reducible]

instance Data.WordOrder.instDecidableEqAffixing : DecidableEq Affixing

Equations

• Data.WordOrder.instDecidableEqAffixing x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Data.WordOrder.instReprAffixing : Repr Affixing

Equations

• Data.WordOrder.instReprAffixing = { reprPrec := Data.WordOrder.instReprAffixing.repr }

def Data.WordOrder.instReprAffixing.repr : Affixing → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.WordOrder.instFintypeAffixing : Fintype Affixing

Equations

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

structure Data.WordOrder.SampleRow : Type

One language of the sample.

• language : String

  The language name as the paper prints it.

• verbPosition : VerbPosition
• adposition : Adposition
• genitive : NounOrder

  The governing noun and its dependent genitive.

• adjective : NounOrder

  The noun and its qualifying adjective.

• demonstrative : NounOrder
• numeral : NounOrder
• rigidVerbFinal : Bool

  The verb follows all its modifiers, with at most object-subject-verb as an alternative order.

• questionParticleSentence : Option SentencePlace

  A yes-no question particle or affix placed by reference to the sentence.

• questionParticleWord : Option Placement

  A yes-no question particle or affix placed by reference to a word.

• questionWordFirst : Bool

  Interrogative words or phrases come first.

• auxiliary : Option Placement

  An inflected auxiliary relative to the main verb.

• adverbAdjective : Option AdverbOrder
• comparison : Option ComparisonOrder
• apposition : Option Apposition
• relative : Option NounOrder

  The nominal antecedent and its relative expression.

• affixing : Affixing

@[instance_reducible]

instance Data.WordOrder.instDecidableEqSampleRow : DecidableEq SampleRow

Equations

• Data.WordOrder.instDecidableEqSampleRow = Data.WordOrder.instDecidableEqSampleRow.decEq

def Data.WordOrder.instDecidableEqSampleRow.decEq (x✝ x✝¹ : SampleRow) : Decidable (x✝ = x✝¹)

Equations

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

def Data.WordOrder.instReprSampleRow.repr : SampleRow → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.WordOrder.instReprSampleRow : Repr SampleRow

Equations

• Data.WordOrder.instReprSampleRow = { reprPrec := Data.WordOrder.instReprSampleRow.repr }

structure Data.WordOrder.OrderType : Type

One of the paper's order types, with the languages the paper lists as attesting it.

• index : ℕ

  The paper's number for the type.

• verbPosition : VerbPosition
• adposition : Adposition
• genitive : NounOrder
• adjective : NounOrder
• attested : List String

def Data.WordOrder.instDecidableEqOrderType.decEq (x✝ x✝¹ : OrderType) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Data.WordOrder.instDecidableEqOrderType : DecidableEq OrderType

Equations

• Data.WordOrder.instDecidableEqOrderType = Data.WordOrder.instDecidableEqOrderType.decEq

@[instance_reducible]

instance Data.WordOrder.instReprOrderType : Repr OrderType

Equations

• Data.WordOrder.instReprOrderType = { reprPrec := Data.WordOrder.instReprOrderType.repr }

def Data.WordOrder.instReprOrderType.repr : OrderType → ℕ → Std.Format

Equations

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