Irish Coordination Morphemes

@cite{haspelmath-2007}

Irish coordination morphemes. Irish is a J-only language for conjunction: "agus" is the sole conjunctive coordinator. There is no MU (additive particle) strategy for conjunction attested.

Connection to Typology.lean: Phenomena.Coordination.Typology.irish encodes the structural pattern (a_co_b only, J-only strategy).

inductive Fragments.Irish.Coordination.CoordRole : Type

Role of a coordination morpheme.

• j : CoordRole
• disj : CoordRole
• advers : CoordRole
• negDisj : CoordRole

instance Fragments.Irish.Coordination.instDecidableEqCoordRole : DecidableEq CoordRole

Equations

• Fragments.Irish.Coordination.instDecidableEqCoordRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Fragments.Irish.Coordination.instBEqCoordRole : BEq CoordRole

Equations

• Fragments.Irish.Coordination.instBEqCoordRole = { beq := Fragments.Irish.Coordination.instBEqCoordRole.beq }

def Fragments.Irish.Coordination.instBEqCoordRole.beq : CoordRole → CoordRole → Bool

Equations

• Fragments.Irish.Coordination.instBEqCoordRole.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.Irish.Coordination.instReprCoordRole.repr : CoordRole → Nat → Std.Format

Equations

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

instance Fragments.Irish.Coordination.instReprCoordRole : Repr CoordRole

Equations

• Fragments.Irish.Coordination.instReprCoordRole = { reprPrec := Fragments.Irish.Coordination.instReprCoordRole.repr }

inductive Fragments.Irish.Coordination.Boundness : Type

Morphological boundness.

• free : Boundness
• bound : Boundness

instance Fragments.Irish.Coordination.instDecidableEqBoundness : DecidableEq Boundness

Equations

• Fragments.Irish.Coordination.instDecidableEqBoundness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Fragments.Irish.Coordination.instBEqBoundness : BEq Boundness

Equations

• Fragments.Irish.Coordination.instBEqBoundness = { beq := Fragments.Irish.Coordination.instBEqBoundness.beq }

def Fragments.Irish.Coordination.instBEqBoundness.beq : Boundness → Boundness → Bool

Equations

• Fragments.Irish.Coordination.instBEqBoundness.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.Irish.Coordination.instReprBoundness.repr : Boundness → Nat → Std.Format

Equations

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

instance Fragments.Irish.Coordination.instReprBoundness : Repr Boundness

Equations

• Fragments.Irish.Coordination.instReprBoundness = { reprPrec := Fragments.Irish.Coordination.instReprBoundness.repr }

structure Fragments.Irish.Coordination.CoordEntry : Type

An Irish coordination entry.

• form : String
• gloss : String
• role : CoordRole
• boundness : Boundness
• note : String

  Additional functions beyond coordination

instance Fragments.Irish.Coordination.instReprCoordEntry : Repr CoordEntry

Equations

• Fragments.Irish.Coordination.instReprCoordEntry = { reprPrec := Fragments.Irish.Coordination.instReprCoordEntry.repr }

def Fragments.Irish.Coordination.instReprCoordEntry.repr : CoordEntry → Nat → Std.Format

Equations

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

instance Fragments.Irish.Coordination.instBEqCoordEntry : BEq CoordEntry

Equations

• Fragments.Irish.Coordination.instBEqCoordEntry = { beq := Fragments.Irish.Coordination.instBEqCoordEntry.beq }

def Fragments.Irish.Coordination.instBEqCoordEntry.beq : CoordEntry → CoordEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Irish.Coordination.instBEqCoordEntry.beq x✝¹ x✝ = false

def Fragments.Irish.Coordination.agus : CoordEntry

agus — conjunction, J particle. Free, prepositive. "Seán agus Máire" = "Seán and Máire".

Equations

• Fragments.Irish.Coordination.agus = { form := "agus", gloss := "and", role := Fragments.Irish.Coordination.CoordRole.j, boundness := Fragments.Irish.Coordination.Boundness.free }

def Fragments.Irish.Coordination.no_ : CoordEntry

nó — disjunction. Free, prepositive. "Seán nó Máire" = "Seán or Máire".

Equations

• Fragments.Irish.Coordination.no_ = { form := "nó", gloss := "or", role := Fragments.Irish.Coordination.CoordRole.disj, boundness := Fragments.Irish.Coordination.Boundness.free }

def Fragments.Irish.Coordination.na_ : CoordEntry

ná — negative disjunction / comparative particle. "ní Seán ná Máire" = "neither Seán nor Máire". Also used in comparatives: "níos mó ná" = "bigger than".

Equations

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

def Fragments.Irish.Coordination.ach : CoordEntry

ach — adversative conjunction. "Tá sé fuar ach tirim" = "It is cold but dry".

Equations

• Fragments.Irish.Coordination.ach = { form := "ach", gloss := "but", role := Fragments.Irish.Coordination.CoordRole.advers, boundness := Fragments.Irish.Coordination.Boundness.free }

def Fragments.Irish.Coordination.allEntries : List CoordEntry

Equations

• Fragments.Irish.Coordination.allEntries = [Fragments.Irish.Coordination.agus, Fragments.Irish.Coordination.no_, Fragments.Irish.Coordination.na_, Fragments.Irish.Coordination.ach]

theorem Fragments.Irish.Coordination.all_free : (allEntries.all fun (x : CoordEntry) => x.boundness == Boundness.free) = true

All Irish coordination morphemes are free (no bound clitics).

theorem Fragments.Irish.Coordination.one_conjunction : (List.filter (fun (x : CoordEntry) => x.role == CoordRole.j) allEntries).length = 1

Irish has exactly one conjunction morpheme (J-only, no MU).