Jacobs2026: statistics (generated)

Auto-generated from Linglib/Data/Statistics/Jacobs2026.json by scripts/gen_statistics.py. Do not edit by hand: edit the JSON and re-run the generator.

Counts of Latialis/Latiaris and linealis/linearis in the Library of Latin Texts, from the combined searches *latiali/*latiale, *latiari/*latiare, *lineale/*lineali and *lineari/*lineare, per period.

References

• [Jac26]

inductive Jacobs2026.Period : Type

The period of a row.

• before200 : Period

  <200: before 200 AD

• from200To500 : Period

  <500: between 200 AD and 500 AD, as the text glosses the row

@[instance_reducible]

instance Jacobs2026.instDecidableEqPeriod : DecidableEq Period

Equations

• Jacobs2026.instDecidableEqPeriod x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Jacobs2026.instReprPeriod : Repr Period

Equations

• Jacobs2026.instReprPeriod = { reprPrec := Jacobs2026.instReprPeriod.repr }

def Jacobs2026.instReprPeriod.repr : Period → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Jacobs2026.instReprPeriod.repr Jacobs2026.Period.before200 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jacobs2026.Period.before200")).group prec✝

@[instance_reducible]

instance Jacobs2026.instFintypePeriod : Fintype Period

Equations

• Jacobs2026.instFintypePeriod = { elems := { val := ↑Jacobs2026.Period.enumList, nodup := Jacobs2026.Period.enumList_nodup }, complete := Jacobs2026.instFintypePeriod._proof_1 }

structure Jacobs2026.HiatusCounts : Type

A row of (23), p. 138: the occurrences of Latialis, Latiaris, linealis and linearis per period.

• latialis : ℕ

  Occurrences of Latialis.

• latiaris : ℕ

  Occurrences of Latiaris.

• linealis : ℕ

  Occurrences of linealis.

• linearis : ℕ

  Occurrences of linearis.

def Jacobs2026.instDecidableEqHiatusCounts.decEq (x✝ x✝¹ : HiatusCounts) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Jacobs2026.instDecidableEqHiatusCounts : DecidableEq HiatusCounts

Equations

• Jacobs2026.instDecidableEqHiatusCounts = Jacobs2026.instDecidableEqHiatusCounts.decEq

@[instance_reducible]

instance Jacobs2026.instReprHiatusCounts : Repr HiatusCounts

Equations

• Jacobs2026.instReprHiatusCounts = { reprPrec := Jacobs2026.instReprHiatusCounts.repr }

def Jacobs2026.instReprHiatusCounts.repr : HiatusCounts → ℕ → Std.Format

Equations

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

def Jacobs2026.table23 : Period → HiatusCounts

The cells of (23), p. 138, by period; counted in a corpus; checked against the page images.

Equations

• Jacobs2026.table23 Jacobs2026.Period.before200 = { latialis := 3, latiaris := 15, linealis := 0, linearis := 7 }
• Jacobs2026.table23 Jacobs2026.Period.from200To500 = { latialis := 3, latiaris := 21, linealis := 1, linearis := 7 }