The member lists of the Levin classes

LevinClass.entry is a class's entry in Part II of Levin's English Verb Classes and Alternations, read from Data/VerbClasses/Levin1993, whose classes come in the book's order, the order of the constructors of LevinClass (number_entry). LevinClass.members are a class's members by citation form, and LevinClass.classesOf the classes whose lists carry a form. An English verb entry's levinClasses are the classes listing its form, less those that list it in a sense the entry does not have, and scripts/check_levin_classes.py checks every entry in CI.

References

• [Lev93]

def ArgumentStructure.LevinClass.entry (c : LevinClass) : Data.VerbClasses.VerbClass

The class's entry in Part II.

Equations

• c.entry = Data.VerbClasses.Levin1993.classes.getD c.ctorIdx default

theorem ArgumentStructure.LevinClass.number_entry (c : LevinClass) : c.entry.number = c.numberString

Each class's entry carries the class's section number.

def ArgumentStructure.LevinClass.members (c : LevinClass) : List String

The class's members by citation form.

Equations

• c.members = c.entry.members

def ArgumentStructure.LevinClass.doubtfulMembers (c : LevinClass) : List String

The members the book marks with a question mark.

Equations

• c.doubtfulMembers = c.entry.doubtful

def ArgumentStructure.LevinClass.classesOf (form : String) : Finset LevinClass

The classes whose member lists carry the form.

Equations

• ArgumentStructure.LevinClass.classesOf form = {x : ArgumentStructure.LevinClass | form ∈ x.members}

@[simp]

theorem ArgumentStructure.LevinClass.mem_classesOf {form : String} {c : LevinClass} : c ∈ classesOf form ↔ form ∈ c.members