Czech noun gender

This file defines the controller genders of Czech. Short counts three genders, "the subcategory of animacy functioning within the masculine only" (p. 465), and agreement treats the masculine animate and the masculine inanimate as two classes: "Agreement with mixed-gender noun phrases (for past tenses and conditional) is dominated in turn by any masculine–animate, masculine–inanimate and feminine" (p. 503), so that Pes a kočka seděli na rohožce 'The dog and the cat were sitting on the mat' takes the masculine animate plural and Dům i stáda byly zničeny 'The house and flocks were destroyed' the masculine inanimate plural. The controller genders are therefore four, and the comparative labels merge the two masculines.

Main definitions

• Czech.Gender.Value: the four controller genders
• Czech.Gender.Value.toLabel: their comparative labels
• Czech.Gender.Value.IsAnimate: the masculine animate

References

• [Sho93a]

inductive Czech.Gender.Value : Type

The controller genders are the masculine animate, the masculine inanimate, the feminine and the neuter, animacy being a subcategory of the masculine alone.

• mascAnimate : Value
• mascInanimate : Value
• feminine : Value
• neuter : Value

@[instance_reducible]

instance Czech.Gender.instDecidableEqValue : DecidableEq Value

Equations

• Czech.Gender.instDecidableEqValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Czech.Gender.instReprValue.repr : Value → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Czech.Gender.instReprValue.repr Czech.Gender.Value.neuter prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Czech.Gender.Value.neuter")).group prec✝

@[instance_reducible]

instance Czech.Gender.instReprValue : Repr Value

Equations

• Czech.Gender.instReprValue = { reprPrec := Czech.Gender.instReprValue.repr }

@[instance_reducible]

instance Czech.Gender.instFintypeValue : Fintype Value

Equations

• Czech.Gender.instFintypeValue = { elems := { val := ↑Czech.Gender.Value.enumList, nodup := Czech.Gender.Value.enumList_nodup }, complete := Czech.Gender.instFintypeValue._proof_1 }

def Czech.Gender.Value.toLabel : Value → Gender

The comparative label of each gender, both masculines being masculine.

Equations

• Czech.Gender.Value.mascAnimate.toLabel = Gender.masculine
• Czech.Gender.Value.mascInanimate.toLabel = Gender.masculine
• Czech.Gender.Value.feminine.toLabel = Gender.feminine
• Czech.Gender.Value.neuter.toLabel = Gender.neuter

def Czech.Gender.Value.IsAnimate (g : Value) : Prop

A gender is animate when it is the masculine animate.

Equations

• g.IsAnimate = (g = Czech.Gender.Value.mascAnimate)

@[instance_reducible]

instance Czech.Gender.instDecidablePredValueIsAnimate : DecidablePred Value.IsAnimate

Equations

• Czech.Gender.instDecidablePredValueIsAnimate g = Czech.Gender.instDecidablePredValueIsAnimate._aux_1 g