Mandarin nouns

The Mandarin noun as a lexical entry: the root entry with the pinyin as citation form, its characters, and the ways a numeral counts it; a name is the root ProperName with its characters. Each noun has its own classifier, and a few have two according to their meaning, shū 'book' taking běn as a thing and bù as a work; beside its own classifiers a noun can always be counted with the general gè (Noun.Takes). A numeral counts a noun that denotes a measure, tiān 'day', without a classifier, and no numeral counts a noun counted through measure words, jiǔ 'wine' or fàn 'cooked rice', in either way. The entries are the pairings of noun and classifier that Li and Thompson and Chao give.

References

• [LT81]
• [Cha68]

structure Mandarin.Nouns.Nounextends ClassifiedNoun Classifier : Type

A Mandarin noun is the root entry with the pinyin as citation form, its characters, and the ways a numeral counts it.

• form : String
• gloss : String
• counters : Finset (Option Classifier)
• hanzi : String

  The characters.

@[instance_reducible]

instance Mandarin.Nouns.instDecidableEqNoun : DecidableEq Noun

Equations

• Mandarin.Nouns.instDecidableEqNoun = Mandarin.Nouns.instDecidableEqNoun.decEq

def Mandarin.Nouns.instDecidableEqNoun.decEq (x✝ x✝¹ : Noun) : Decidable (x✝ = x✝¹)

Equations

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

def Mandarin.Nouns.Noun.Takes (n : Noun) (c : Classifier) : Prop

A noun can be counted with a classifier of its own, and with the general gè when it takes a classifier at all.

Equations

• n.Takes c = (c ∈ n.classifiers ∨ c = Mandarin.Classifiers.ge ∧ n.classifiers.Nonempty)

@[instance_reducible]

instance Mandarin.Nouns.instDecidableTakes (n : Noun) (c : Classifier) : Decidable (n.Takes c)

Equations

• Mandarin.Nouns.instDecidableTakes n c = { decide := decide (c ∈ n.classifiers) || decide (c = Mandarin.Classifiers.ge ∧ n.classifiers.Nonempty), reflects_decide := ⋯ }

theorem Mandarin.Nouns.Noun.takes_ge {n : Noun} (h : n.classifiers.Nonempty) : n.Takes Classifiers.ge

A noun that takes a classifier can be counted with gè.

theorem Mandarin.Nouns.Noun.not_takes_of_eq_empty {n : Noun} (h : n.classifiers = ∅) (c : Classifier) : ¬n.Takes c

A noun that takes no classifier takes none.

Nouns counted with gè alone

def Mandarin.Nouns.ren : Noun

人 rén 'person'.

Equations

• Mandarin.Nouns.ren = { form := "rén", gloss := "person", counters := {some Mandarin.Classifiers.ge}, hanzi := "人" }

def Mandarin.Nouns.wenti : Noun

问题 wèntí 'problem'.

Equations

• Mandarin.Nouns.wenti = { form := "wèntí", gloss := "problem", counters := {some Mandarin.Classifiers.ge}, hanzi := "问题" }

Nouns with a classifier of their own

def Mandarin.Nouns.xiansheng : Noun

先生 xiānsheng 'gentleman', counted with the polite wèi.

Equations

• Mandarin.Nouns.xiansheng = { form := "xiānsheng", gloss := "gentleman", counters := {some Mandarin.Classifiers.wei}, hanzi := "先生" }

def Mandarin.Nouns.gou : Noun

狗 gǒu 'dog', with zhī and, in some dialects, tiáo.

Equations

• Mandarin.Nouns.gou = { form := "gǒu", gloss := "dog", counters := {some Mandarin.Classifiers.zhi, some Mandarin.Classifiers.tiao}, hanzi := "狗" }

def Mandarin.Nouns.shou : Noun

手 shǒu 'hand'.

Equations

• Mandarin.Nouns.shou = { form := "shǒu", gloss := "hand", counters := {some Mandarin.Classifiers.zhi}, hanzi := "手" }

def Mandarin.Nouns.yifu : Noun

衣服 yīfu 'garment'.

Equations

• Mandarin.Nouns.yifu = { form := "yīfu", gloss := "garment", counters := {some Mandarin.Classifiers.jian}, hanzi := "衣服" }

def Mandarin.Nouns.hua : Noun

花 huā 'flower', with duǒ for the blossom and kē for the plant.

Equations

• Mandarin.Nouns.hua = { form := "huā", gloss := "flower", counters := {some Mandarin.Classifiers.duo, some Mandarin.Classifiers.ke}, hanzi := "花" }

def Mandarin.Nouns.cao : Noun

草 cǎo 'grass'.

Equations

• Mandarin.Nouns.cao = { form := "cǎo", gloss := "grass", counters := {some Mandarin.Classifiers.ke}, hanzi := "草" }

def Mandarin.Nouns.feiji : Noun

飞机 fēijī 'airplane'.

Equations

• Mandarin.Nouns.feiji = { form := "fēijī", gloss := "airplane", counters := {some Mandarin.Classifiers.jia}, hanzi := "飞机" }

def Mandarin.Nouns.che : Noun

车 chē 'vehicle'.

Equations

• Mandarin.Nouns.che = { form := "chē", gloss := "vehicle", counters := {some Mandarin.Classifiers.liang}, hanzi := "车" }

def Mandarin.Nouns.deng : Noun

灯 dēng 'lamp'.

Equations

• Mandarin.Nouns.deng = { form := "dēng", gloss := "lamp", counters := {some Mandarin.Classifiers.zhan}, hanzi := "灯" }

def Mandarin.Nouns.ma : Noun

马 mǎ 'horse'.

Equations

• Mandarin.Nouns.ma = { form := "mǎ", gloss := "horse", counters := {some Mandarin.Classifiers.pi}, hanzi := "马" }

def Mandarin.Nouns.niu : Noun

牛 niú 'cattle, cow', with tóu and tiáo.

Equations

• Mandarin.Nouns.niu = { form := "niú", gloss := "cattle", counters := {some Mandarin.Classifiers.tou, some Mandarin.Classifiers.tiao}, hanzi := "牛" }

def Mandarin.Nouns.shu : Noun

书 shū 'book', with běn for the thing and bù for the work.

Equations

• Mandarin.Nouns.shu = { form := "shū", gloss := "book", counters := {some Mandarin.Classifiers.ben, some Mandarin.Classifiers.bu}, hanzi := "书" }

def Mandarin.Nouns.chuang : Noun

床 chuáng 'bed'.

Equations

• Mandarin.Nouns.chuang = { form := "chuáng", gloss := "bed", counters := {some Mandarin.Classifiers.zhang}, hanzi := "床" }

def Mandarin.Nouns.zhuozi : Noun

桌子 zhuōzi 'table'.

Equations

• Mandarin.Nouns.zhuozi = { form := "zhuōzi", gloss := "table", counters := {some Mandarin.Classifiers.zhang}, hanzi := "桌子" }

def Mandarin.Nouns.dao : Noun

刀 dāo 'knife'.

Equations

• Mandarin.Nouns.dao = { form := "dāo", gloss := "knife", counters := {some Mandarin.Classifiers.ba}, hanzi := "刀" }

def Mandarin.Nouns.maobi : Noun

毛笔 máobǐ 'brush-pen', elongated but counted with zhī 枝 rather than tiáo.

Equations

• Mandarin.Nouns.maobi = { form := "máobǐ", gloss := "brush-pen", counters := {some Mandarin.Classifiers.zhiBranch}, hanzi := "毛笔" }

def Mandarin.Nouns.jian : Noun

箭 jiàn 'arrow', elongated but counted with zhī 枝 rather than tiáo.

Equations

• Mandarin.Nouns.jian = { form := "jiàn", gloss := "arrow", counters := {some Mandarin.Classifiers.zhiBranch}, hanzi := "箭" }

def Mandarin.Nouns.she : Noun

蛇 shé 'snake'.

Equations

• Mandarin.Nouns.she = { form := "shé", gloss := "snake", counters := {some Mandarin.Classifiers.tiao}, hanzi := "蛇" }

def Mandarin.Nouns.yu : Noun

鱼 yú 'fish'.

Equations

• Mandarin.Nouns.yu = { form := "yú", gloss := "fish", counters := {some Mandarin.Classifiers.tiao}, hanzi := "鱼" }

def Mandarin.Nouns.shengzi : Noun

绳子 shéngzi 'rope'.

Equations

• Mandarin.Nouns.shengzi = { form := "shéngzi", gloss := "rope", counters := {some Mandarin.Classifiers.tiao}, hanzi := "绳子" }

def Mandarin.Nouns.lu : Noun

路 lù 'road'.

Equations

• Mandarin.Nouns.lu = { form := "lù", gloss := "road", counters := {some Mandarin.Classifiers.tiao}, hanzi := "路" }

def Mandarin.Nouns.he : Noun

河 hé 'river', with tiáo and dào.

Equations

• Mandarin.Nouns.he = { form := "hé", gloss := "river", counters := {some Mandarin.Classifiers.tiao, some Mandarin.Classifiers.dao}, hanzi := "河" }

def Mandarin.Nouns.xinwen : Noun

新闻 xīnwén 'news', counted with tiáo though not elongated.

Equations

• Mandarin.Nouns.xinwen = { form := "xīnwén", gloss := "news", counters := {some Mandarin.Classifiers.tiao}, hanzi := "新闻" }

def Mandarin.Nouns.falu : Noun

法律 fǎlǜ 'law', counted with tiáo though not elongated.

Equations

• Mandarin.Nouns.falu = { form := "fǎlǜ", gloss := "law", counters := {some Mandarin.Classifiers.tiao}, hanzi := "法律" }

def Mandarin.Nouns.cai : Noun

菜 cài 'course of food', counted with dào.

Equations

• Mandarin.Nouns.cai = { form := "cài", gloss := "course of food", counters := {some Mandarin.Classifiers.dao}, hanzi := "菜" }

def Mandarin.Nouns.dapao : Noun

大炮 dàpào 'artillery piece'.

Equations

• Mandarin.Nouns.dapao = { form := "dàpào", gloss := "artillery piece", counters := {some Mandarin.Classifiers.men}, hanzi := "大炮" }

Nouns with no classifier

def Mandarin.Nouns.tian : Noun

天 tiān 'day' denotes a measure and is counted without a classifier, sān tiān 'three days', not sān ge tiān.

Equations

• Mandarin.Nouns.tian = { form := "tiān", gloss := "day", counters := {none}, hanzi := "天" }

def Mandarin.Nouns.jiu : Noun

酒 jiǔ 'wine' is counted through a measure word, bēi jiǔ 'glasses of wine'.

Equations

• Mandarin.Nouns.jiu = { form := "jiǔ", gloss := "wine", counters := ∅, hanzi := "酒" }

def Mandarin.Nouns.fan : Noun

饭 fàn 'cooked rice' is counted through a measure word, yī guō fàn 'a pot of rice'.

Equations

• Mandarin.Nouns.fan = { form := "fàn", gloss := "cooked rice", counters := ∅, hanzi := "饭" }

def Mandarin.Nouns.nouns : List Noun

The nouns.

Equations

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

theorem Mandarin.Nouns.not_takes_tian (c : Classifier) : ¬tian.Takes c

Sān ge tiān is out: tiān takes no classifier, not even gè.

Proper names

structure Mandarin.Nouns.ProperNameextends ProperName : Type

A Mandarin name is the root name with the pinyin as citation form, and its characters.

• form : String
• gloss : String
• gender : Option Gender
• hanzi : String

  The characters.

@[instance_reducible]

instance Mandarin.Nouns.instDecidableEqProperName : DecidableEq ProperName

Equations

• Mandarin.Nouns.instDecidableEqProperName = Mandarin.Nouns.instDecidableEqProperName.decEq

def Mandarin.Nouns.instDecidableEqProperName.decEq (x✝ x✝¹ : ProperName) : Decidable (x✝ = x✝¹)

Equations

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

def Mandarin.Nouns.instReprProperName.repr : ProperName → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Mandarin.Nouns.instReprProperName : Repr ProperName

Equations

• Mandarin.Nouns.instReprProperName = { reprPrec := Mandarin.Nouns.instReprProperName.repr }

def Mandarin.Nouns.name (form hanzi : String) : ProperName

A personal name glossed by its pinyin.

Equations

• Mandarin.Nouns.name form hanzi = { form := form, gloss := form, hanzi := hanzi }

def Mandarin.Nouns.zhangsan : ProperName

Equations

• Mandarin.Nouns.zhangsan = Mandarin.Nouns.name "Zhāngsān" "张三"

def Mandarin.Nouns.lisi : ProperName

Equations

• Mandarin.Nouns.lisi = Mandarin.Nouns.name "Lǐsì" "李四"

def Mandarin.Nouns.xiaoming : ProperName

Equations

• Mandarin.Nouns.xiaoming = Mandarin.Nouns.name "Xiǎomíng" "小明"