Zürich German case

This file defines the cases of Shieber's Zürich German clauses: the nominative of a subject such as mer 'we', and the accusative and the dative of the objects, which the article tells apart, de Hans against em Hans (Shieber's (3)–(4)), as articleCase records.

Implementation notes

The cases are those the clauses mark, and no other case of the dialect is recorded.

References

• [Shi85]

inductive German.Zurich.Case : Type

The cases of the clauses.

• nom : Case

  The nominative.

• acc : Case

  The accusative.

• dat : Case

  The dative.

@[instance_reducible]

instance German.Zurich.instDecidableEqCase : DecidableEq Case

Equations

• German.Zurich.instDecidableEqCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance German.Zurich.instFintypeCase : Fintype Case

Equations

• German.Zurich.instFintypeCase = { elems := { val := ↑German.Zurich.Case.enumList, nodup := German.Zurich.Case.enumList_nodup }, complete := German.Zurich.instFintypeCase._proof_1 }

@[instance_reducible]

instance German.Zurich.instReprCase : Repr Case

Equations

• German.Zurich.instReprCase = { reprPrec := German.Zurich.instReprCase.repr }

def German.Zurich.instReprCase.repr : Case → ℕ → Std.Format

Equations

• German.Zurich.instReprCase.repr German.Zurich.Case.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "German.Zurich.Case.nom")).group prec✝
• German.Zurich.instReprCase.repr German.Zurich.Case.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "German.Zurich.Case.acc")).group prec✝
• German.Zurich.instReprCase.repr German.Zurich.Case.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "German.Zurich.Case.dat")).group prec✝

def German.Zurich.Case.label : Case → _root_.Case

The comparative value a case is named for.

Equations

• German.Zurich.Case.nom.label = Case.nom
• German.Zurich.Case.acc.label = Case.acc
• German.Zurich.Case.dat.label = Case.dat

def German.Zurich.articleCase : List (String × Case)

The articles of the clauses' objects and the case each marks: em the dative, and de, es and the clitic d' the accusative.

Equations

• German.Zurich.articleCase = [("em", German.Zurich.Case.dat), ("de", German.Zurich.Case.acc), ("es", German.Zurich.Case.acc), ("d'", German.Zurich.Case.acc)]