Basel German case #

This file defines the three cases of Basel German, nominative, accusative and dative, with the forms of the definite article and of the stressed first person singular pronoun, following Suter's grammar. The personal pronouns keep all three cases apart (§124). The article marks the dative, but it never tells the accusative from the nominative, so that the accusative differs from the nominative on nouns only by position in the clause (§82). The genitive has long vanished as a case (§91), and the possessor is a dative, with a possessive pronoun or after vo (§193).

Main declarations #

German.Basel.Case: the three cases.
German.Basel.article, German.Basel.pronoun: the forms of the definite article in each gender and number (§83), and of the stressed first person singular pronoun (§125).
article_nom_eq_acc, article_dat_ne_nom, pronoun_injective: the article marks the dative but not the accusative, and the pronoun marks both.

Implementation notes #

A cell holds all the forms Suter gives for it: the article d beside its full form die, and the stressed yy beside yych. The genitive article s of names for a whole family, s Waagners 'the Wagner family' (§83), and the forms am and im heard beside the dative em (§85) are left out.

References #

[Sut92]

source

inductive German.Basel.Case :

Type

The three cases.

nom : Case
The nominative.
acc : Case
The accusative.
dat : Case
The dative.

Instances For

source

@[instance_reducible]

instance German.Basel.instDecidableEqCase :

DecidableEq Case

Equations

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

source

@[instance_reducible]

instance German.Basel.instFintypeCase :

Fintype Case

Equations

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

source

@[instance_reducible]

instance German.Basel.instReprCase :

Repr Case

Equations

German.Basel.instReprCase = { reprPrec := German.Basel.instReprCase.repr }

source

def German.Basel.instReprCase.repr :

Case → ℕ → Std.Format

Equations

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

Instances For

source

def German.Basel.Case.label :

Case → _root_.Case

The comparative value a case is named for.

Equations

Instances For

source

def German.Basel.article :

Determiners.GenderNumber → Case → Finset String

The forms of the definite article (§83): der in the masculine and s in the neuter nominative and accusative singular, d or die in the feminine singular and the plural, em in the masculine and neuter dative singular, der in the feminine and de in the plural.

Equations