def Phenomena.Generics.KindReference.containsSubstr (s sub : String) : Bool

Check if a string contains a substring

Equations

• Phenomena.Generics.KindReference.containsSubstr s sub = decide ((s.splitOn sub).length > 1)

inductive Phenomena.Generics.KindReference.BareNominalType : Type

Language typology for bare nominal licensing.

• barePluralOnly : BareNominalType
• definiteRequired : BareNominalType
• fullyBare : BareNominalType
• classifier : BareNominalType

instance Phenomena.Generics.KindReference.instReprBareNominalType : Repr BareNominalType

Equations

• Phenomena.Generics.KindReference.instReprBareNominalType = { reprPrec := Phenomena.Generics.KindReference.instReprBareNominalType.repr }

def Phenomena.Generics.KindReference.instReprBareNominalType.repr : BareNominalType → Nat → Std.Format

Equations

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

instance Phenomena.Generics.KindReference.instDecidableEqBareNominalType : DecidableEq BareNominalType

Equations

• Phenomena.Generics.KindReference.instDecidableEqBareNominalType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Generics.KindReference.instBEqBareNominalType : BEq BareNominalType

Equations

• Phenomena.Generics.KindReference.instBEqBareNominalType = { beq := Phenomena.Generics.KindReference.instBEqBareNominalType.beq }

def Phenomena.Generics.KindReference.instBEqBareNominalType.beq : BareNominalType → BareNominalType → Bool

Equations

• Phenomena.Generics.KindReference.instBEqBareNominalType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.Generics.KindReference.CrossLingDatum : Type

Cross-linguistic kind reference datum.

• language : String
• nominalType : BareNominalType
• sentence : String
• gloss : String
• bareKindOK : Bool
• defKindOK : Bool
• bareSgKindOK : Bool
• notes : String

def Phenomena.Generics.KindReference.englishBarePlural : CrossLingDatum

Equations

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

def Phenomena.Generics.KindReference.englishDefiniteSingularKind : CrossLingDatum

Equations

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

def Phenomena.Generics.KindReference.englishMassNoun : CrossLingDatum

Equations

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

def Phenomena.Generics.KindReference.frenchPluralKind : CrossLingDatum

Equations

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

def Phenomena.Generics.KindReference.frenchSingularKind : CrossLingDatum

Equations

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

def Phenomena.Generics.KindReference.hindiKind : CrossLingDatum

Equations

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

def Phenomena.Generics.KindReference.hindiDefiniteContext : CrossLingDatum

Equations

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

def Phenomena.Generics.KindReference.russianKind : CrossLingDatum

Equations

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

def Phenomena.Generics.KindReference.mandarinKind : CrossLingDatum

Equations

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

structure Phenomena.Generics.KindReference.BareSingularDatum : Type

Bare singular grammaticality datum

• sentence : String
• grammatical : Bool
• npType : String
• position : String
• notes : String

def Phenomena.Generics.KindReference.bareSgSubject : BareSingularDatum

Equations

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

def Phenomena.Generics.KindReference.barePlSubject : BareSingularDatum

Equations

• Phenomena.Generics.KindReference.barePlSubject = { sentence := "Dogs bark", grammatical := true, npType := "bare pl", position := "subject", notes := "Bare plural OK" }

def Phenomena.Generics.KindReference.bareMassSubject : BareSingularDatum

Equations

• Phenomena.Generics.KindReference.bareMassSubject = { sentence := "Water is wet", grammatical := true, npType := "bare mass", position := "subject", notes := "Bare mass noun OK" }

def Phenomena.Generics.KindReference.bareSgObject : BareSingularDatum

Equations

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

def Phenomena.Generics.KindReference.barePlObject : BareSingularDatum

Equations

• Phenomena.Generics.KindReference.barePlObject = { sentence := "I saw dogs", grammatical := true, npType := "bare pl", position := "object", notes := "Bare plural OK as object" }

structure Phenomena.Generics.KindReference.ScopeDatum : Type

Scope ambiguity datum

• sentence : String
• ambiguous : Bool

  Is the object NP scopally ambiguous?

• narrowScope : String

  Available readings

• wideScope : Option String
• notes : String

def Phenomena.Generics.KindReference.negationBarePlural : ScopeDatum

Equations

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

def Phenomena.Generics.KindReference.negationSomeDogs : ScopeDatum

Equations

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

def Phenomena.Generics.KindReference.universalBarePlural : ScopeDatum

Equations

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

def Phenomena.Generics.KindReference.universalSomeBooks : ScopeDatum

Equations

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

inductive Phenomena.Generics.KindReference.ScramblingPosition : Type

Scrambling position.

• unscrambled : ScramblingPosition
• scrambled : ScramblingPosition

instance Phenomena.Generics.KindReference.instReprScramblingPosition : Repr ScramblingPosition

Equations

• Phenomena.Generics.KindReference.instReprScramblingPosition = { reprPrec := Phenomena.Generics.KindReference.instReprScramblingPosition.repr }

def Phenomena.Generics.KindReference.instReprScramblingPosition.repr : ScramblingPosition → Nat → Std.Format

Equations

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

instance Phenomena.Generics.KindReference.instDecidableEqScramblingPosition : DecidableEq ScramblingPosition

Equations

• Phenomena.Generics.KindReference.instDecidableEqScramblingPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Generics.KindReference.instBEqScramblingPosition : BEq ScramblingPosition

Equations

• Phenomena.Generics.KindReference.instBEqScramblingPosition = { beq := Phenomena.Generics.KindReference.instBEqScramblingPosition.beq }

def Phenomena.Generics.KindReference.instBEqScramblingPosition.beq : ScramblingPosition → ScramblingPosition → Bool

Equations

• Phenomena.Generics.KindReference.instBEqScramblingPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.Generics.KindReference.ScramblingScopeDatum : Type

Scrambling scope datum.

• sentence : String
• language : String
• gloss : Option String
• translation : String
• position : ScramblingPosition
• narrowOK : Bool
• wideOK : Bool
• kindReferenceOK : Bool
• notes : String

def Phenomena.Generics.KindReference.dutchUnscrambledNeg : ScramblingScopeDatum

Equations

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

def Phenomena.Generics.KindReference.dutchScrambledMensen : ScramblingScopeDatum

Equations

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

def Phenomena.Generics.KindReference.dutchScrambledBoeken : ScramblingScopeDatum

Equations

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

def Phenomena.Generics.KindReference.dutchScrambledKindMensen : ScramblingScopeDatum

Equations

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

def Phenomena.Generics.KindReference.dutchScrambledKindBoeken : ScramblingScopeDatum

Equations

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

def Phenomena.Generics.KindReference.germanScrambledKomponenten : ScramblingScopeDatum

Equations

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

def Phenomena.Generics.KindReference.germanScrambledMenschen : ScramblingScopeDatum

Equations

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

def Phenomena.Generics.KindReference.modifiedBPwideScope : ScramblingScopeDatum

Equations

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

def Phenomena.Generics.KindReference.scramblingData : List ScramblingScopeDatum

Equations

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

inductive Phenomena.Generics.KindReference.PredLevel : Type

Predicate type for kind application

• kind : PredLevel

  Applies directly to kinds: extinct, widespread, evolve

• object : PredLevel

  Applies to individuals; needs coercion for kinds: bark, sleep

def Phenomena.Generics.KindReference.instReprPredLevel.repr : PredLevel → Nat → Std.Format

Equations

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

instance Phenomena.Generics.KindReference.instReprPredLevel : Repr PredLevel

Equations

• Phenomena.Generics.KindReference.instReprPredLevel = { reprPrec := Phenomena.Generics.KindReference.instReprPredLevel.repr }

instance Phenomena.Generics.KindReference.instDecidableEqPredLevel : DecidableEq PredLevel

Equations

• Phenomena.Generics.KindReference.instDecidableEqPredLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Generics.KindReference.instBEqPredLevel.beq : PredLevel → PredLevel → Bool

Equations

• Phenomena.Generics.KindReference.instBEqPredLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.KindReference.instBEqPredLevel : BEq PredLevel

Equations

• Phenomena.Generics.KindReference.instBEqPredLevel = { beq := Phenomena.Generics.KindReference.instBEqPredLevel.beq }

structure Phenomena.Generics.KindReference.PredicateDatum : Type

Predicate classification datum

• predicate : String
• level : PredLevel
• exampleSentence : String
• directKindApplication : Bool

  Does it apply directly to kind-denoting NP?

• notes : String

def Phenomena.Generics.KindReference.beExtinct : PredicateDatum

Equations

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

def Phenomena.Generics.KindReference.beWidespread : PredicateDatum

Equations

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

def Phenomena.Generics.KindReference.beRare : PredicateDatum

Equations

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

def Phenomena.Generics.KindReference.evolveFrom : PredicateDatum

Equations

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

def Phenomena.Generics.KindReference.beInvented : PredicateDatum

Equations

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

def Phenomena.Generics.KindReference.beBarkingInYard : PredicateDatum

Equations

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

def Phenomena.Generics.KindReference.beInGarden : PredicateDatum

Equations

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

inductive Phenomena.Generics.KindReference.SingularKindLicense : Type

Type of singular kind licensing

• extinct : SingularKindLicense

  Extinct - no instances to distinguish

• invention : SingularKindLicense

  Invention/artifact - conceptualized as atomic

• taxonomic : SingularKindLicense

  Taxonomic - species-level predication

instance Phenomena.Generics.KindReference.instReprSingularKindLicense : Repr SingularKindLicense

Equations

• Phenomena.Generics.KindReference.instReprSingularKindLicense = { reprPrec := Phenomena.Generics.KindReference.instReprSingularKindLicense.repr }

def Phenomena.Generics.KindReference.instReprSingularKindLicense.repr : SingularKindLicense → Nat → Std.Format

Equations

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

instance Phenomena.Generics.KindReference.instDecidableEqSingularKindLicense : DecidableEq SingularKindLicense

Equations

• Phenomena.Generics.KindReference.instDecidableEqSingularKindLicense x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Generics.KindReference.instBEqSingularKindLicense.beq : SingularKindLicense → SingularKindLicense → Bool

Equations

• Phenomena.Generics.KindReference.instBEqSingularKindLicense.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.KindReference.instBEqSingularKindLicense : BEq SingularKindLicense

Equations

• Phenomena.Generics.KindReference.instBEqSingularKindLicense = { beq := Phenomena.Generics.KindReference.instBEqSingularKindLicense.beq }

structure Phenomena.Generics.KindReference.SingularKindDatum : Type

Singular kind datum

• sentence : String
• np : String
• license : SingularKindLicense
• grammatical : Bool
• notes : String

def Phenomena.Generics.KindReference.dodoExtinct : SingularKindDatum

Equations

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

def Phenomena.Generics.KindReference.computerRevolutionized : SingularKindDatum

Equations

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

def Phenomena.Generics.KindReference.lionPredator : SingularKindDatum

Equations

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

def Phenomena.Generics.KindReference.whaleEndangered : SingularKindDatum

Equations

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

def Phenomena.Generics.KindReference.tallLionOdd : SingularKindDatum

Equations

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

structure Phenomena.Generics.KindReference.TaxonomicDatum : Type

Taxonomic reading datum

• sentence : String
• taxonomicOK : Bool

  Is taxonomic (sub-kind) reading available?

• individualOK : Bool

  Is individual reading available?

• notes : String

def Phenomena.Generics.KindReference.dogEvolvedWolf : TaxonomicDatum

Equations

• Phenomena.Generics.KindReference.dogEvolvedWolf = { sentence := "The dog evolved from the wolf", taxonomicOK := true, individualOK := false, notes := "Only taxonomic makes sense" }

def Phenomena.Generics.KindReference.dogSleeping : TaxonomicDatum

Equations

• Phenomena.Generics.KindReference.dogSleeping = { sentence := "The dog is sleeping", taxonomicOK := false, individualOK := true, notes := "Only individual reading" }

def Phenomena.Generics.KindReference.dogMammal : TaxonomicDatum

Equations

• Phenomena.Generics.KindReference.dogMammal = { sentence := "The dog is a mammal", taxonomicOK := true, individualOK := true, notes := "Ambiguous: kind or individual" }

inductive Phenomena.Generics.KindReference.NominalDenotation : Type

Denotation type for bare nominal expressions.

• kind : NominalDenotation

  Denotes a kind (individual concept, type e)

• property : NominalDenotation

  Denotes a property (type ⟨e,t⟩)

def Phenomena.Generics.KindReference.instReprNominalDenotation.repr : NominalDenotation → Nat → Std.Format

Equations

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

instance Phenomena.Generics.KindReference.instReprNominalDenotation : Repr NominalDenotation

Equations

• Phenomena.Generics.KindReference.instReprNominalDenotation = { reprPrec := Phenomena.Generics.KindReference.instReprNominalDenotation.repr }

instance Phenomena.Generics.KindReference.instDecidableEqNominalDenotation : DecidableEq NominalDenotation

Equations

• Phenomena.Generics.KindReference.instDecidableEqNominalDenotation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Generics.KindReference.instBEqNominalDenotation.beq : NominalDenotation → NominalDenotation → Bool

Equations

• Phenomena.Generics.KindReference.instBEqNominalDenotation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.KindReference.instBEqNominalDenotation : BEq NominalDenotation

Equations

• Phenomena.Generics.KindReference.instBEqNominalDenotation = { beq := Phenomena.Generics.KindReference.instBEqNominalDenotation.beq }

structure Phenomena.Generics.KindReference.BPDenotationDatum : Type

English bare plural denotation ambiguity datum.

@cite{guerrini-2026} argues that English BPs are systematically ambiguous between kind and property denotation. The kind reading feeds Distributive/Cumulative Kind Predication; the property reading feeds Bona Fide Generic LFs or low-scoped existential LFs (via DPP).

Italian disambiguates: definite plurals = kind only; bare plurals = property only.

• language : String
• form : String
• denotation : NominalDenotation
• available : Bool
• lfConsequence : String
• notes : String

def Phenomena.Generics.KindReference.englishBPKind : BPDenotationDatum

Equations

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

def Phenomena.Generics.KindReference.englishBPProperty : BPDenotationDatum

Equations

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

def Phenomena.Generics.KindReference.italianDefPlKind : BPDenotationDatum

Equations

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

def Phenomena.Generics.KindReference.italianDefPlProperty : BPDenotationDatum

Equations

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

def Phenomena.Generics.KindReference.italianBarePlKind : BPDenotationDatum

Equations

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

def Phenomena.Generics.KindReference.italianBarePlProperty : BPDenotationDatum

Equations

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

def Phenomena.Generics.KindReference.bpDenotationData : List BPDenotationDatum

Equations

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

def Phenomena.Generics.KindReference.crossLingData : List CrossLingDatum

Equations

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

def Phenomena.Generics.KindReference.bareSingularData : List BareSingularDatum

Equations

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

def Phenomena.Generics.KindReference.scopeData : List ScopeDatum

Equations

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

def Phenomena.Generics.KindReference.predicateData : List PredicateDatum

Equations

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

def Phenomena.Generics.KindReference.singularKindData : List SingularKindDatum

Equations

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