Complementation data schema

Typed schema for cross-linguistic complement-taking-predicate (CTP) rows, the home of the canonical sample behind [Noo07]. Generated rows live in Data/Complementation/<Paper>.lean, emitted from the canonical <Paper>.json by scripts/gen_complementation.py.

This is substrate: it imports Features/Complementation.lean only. Consumers (the paper's study file, bridge studies) import the generated module.

Main definitions

• Datum — one CTP row: verb, CTP class, attested complement codings, equi-deletion, negative raising.

structure Data.Complementation.Datum : Type

One row of [Noo07]'s sample: a complement-taking predicate in one language, with its predicate class, the complement codings it is attested with, and its equi-deletion and negative-raising behavior. verb is citation provenance, not identity; rows are identified by their generated names and grouped into per-language lists, and a row's reality status is Complement.PredicateClass.realityStatus of its class.

• verb : String
• predicateClass : Complement.PredicateClass
• codings : List Complement.Coding
• hasEquiDeletion : Bool
• hasNegativeRaising : Bool

def Data.Complementation.instDecidableEqDatum.decEq (x✝ x✝¹ : Datum) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Data.Complementation.instDecidableEqDatum : DecidableEq Datum

Equations

• Data.Complementation.instDecidableEqDatum = Data.Complementation.instDecidableEqDatum.decEq

def Data.Complementation.instReprDatum.repr : Datum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Data.Complementation.instReprDatum : Repr Datum

Equations

• Data.Complementation.instReprDatum = { reprPrec := Data.Complementation.instReprDatum.repr }