Animacy

The animacy of a referent places it on the scale human > animate > inanimate, the animacy hierarchy proper. Corbett reads the wider hierarchies that govern number marking, which put the personal pronouns above all nouns, as this scale combined with a person scale and the distinction between pronouns and nouns, after Comrie; Aissen crosses it with definiteness to state differential object marking.

References

• [Ais03]
• [Com89]
• [Cor00]

inductive Reference.Animacy : Type

The animacy of a referent ranks the human above the non-human animate above the inanimate, as on Aissen's animacy scale and Corbett's animacy hierarchy proper.

• inanimate : Animacy
• animate : Animacy

  Non-human animates, Comrie's and Haspelmath's animal.

• human : Animacy

@[instance_reducible]

instance Reference.instDecidableEqAnimacy : DecidableEq Animacy

Equations

• Reference.instDecidableEqAnimacy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Reference.instReprAnimacy : Repr Animacy

Equations

• Reference.instReprAnimacy = { reprPrec := Reference.instReprAnimacy.repr }

def Reference.instReprAnimacy.repr : Animacy → ℕ → Std.Format

Equations

• Reference.instReprAnimacy.repr Reference.Animacy.inanimate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reference.Animacy.inanimate")).group prec✝
• Reference.instReprAnimacy.repr Reference.Animacy.animate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reference.Animacy.animate")).group prec✝
• Reference.instReprAnimacy.repr Reference.Animacy.human prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Reference.Animacy.human")).group prec✝

@[instance_reducible]

instance Reference.instFintypeAnimacy : Fintype Animacy

Equations

• Reference.instFintypeAnimacy = { elems := { val := ↑Reference.Animacy.enumList, nodup := Reference.Animacy.enumList_nodup }, complete := Reference.instFintypeAnimacy._proof_1 }

def Reference.Animacy.rank : Animacy → ℕ

The rank on the scale, 0 for the inanimate, 1 for the animate and 2 for the human.

Equations

• Reference.Animacy.inanimate.rank = 0
• Reference.Animacy.animate.rank = 1
• Reference.Animacy.human.rank = 2

@[instance_reducible]

instance Reference.Animacy.instLinearOrder : LinearOrder Animacy

Equations

• Reference.Animacy.instLinearOrder = LinearOrder.lift' Reference.Animacy.rank Reference.Animacy.instLinearOrder._proof_1

def Reference.Animacy.all : List Animacy

The animacies, most animate first.

Equations

• Reference.Animacy.all = [Reference.Animacy.human, Reference.Animacy.animate, Reference.Animacy.inanimate]