Additive particles

An additive particle is a focus particle meaning 'also, too', English too in Mary is well too. Such particles often also mean 'and': Japanese mo is 'too' after one phrase and 'and' after each of two conjuncts, and Haspelmath counts the additive particle among the two main sources of conjunction. This file defines the lexical record of an additive particle, whose meaning is Focus.Particles.additive; a coordinator whose form is that of an additive particle is Coordinator.IsAlsoAdditive.

Main definitions

• AdditiveParticle: the form and gloss of an additive particle.

References

• [Has97]
• [Has07]
• [MS16a]

structure AdditiveParticle : Type

An additive particle of a language is a focus particle meaning 'also, too'.

• morph : Morphology.Morph

  The form, a free word or a clitic.

• gloss : String

  The gloss.

def instDecidableEqAdditiveParticle.decEq (x✝ x✝¹ : AdditiveParticle) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqAdditiveParticle.decEq { morph := a, gloss := a_1 } { morph := b, gloss := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance instDecidableEqAdditiveParticle : DecidableEq AdditiveParticle

Equations

• instDecidableEqAdditiveParticle = instDecidableEqAdditiveParticle.decEq

def instReprAdditiveParticle.repr : AdditiveParticle → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance instReprAdditiveParticle : Repr AdditiveParticle

Equations

• instReprAdditiveParticle = { reprPrec := instReprAdditiveParticle.repr }