Construction Grammar: Core Types

[Gol95] [Gol03] [Gol06] [KF99] [Dun25]

Constructions — learned pairings of form and function — are the basic units of grammatical knowledge in CxG. The form side is typed: a TypedForm is a sequence of Slots, each fixing a lexeme, opening a category, or admitting any phrase ([Dun25]'s LEX/SYN/SEM+ representation levels, plus [KF99]'s grammatical functions, coreference indices, and slot constraints). Abstraction measures and Specificity are derived from the slot structure (Construction.specificity), not stipulated.

A slot also records the bar level of its position; a phrasal filler in a zero-level position (Slot.IsPhraseInWordSlot) is the phrase-in-word-slot configuration of phrasal compounds and the PAL construction.

Main declarations

• SlotFiller, Slot, TypedForm: the typed form side
• abstractionLevel, derivedSpecificity: abstraction measures on forms
• Construction, Construction.specificity: form–function pairings
• InheritanceLink, Constructicon: the network

inductive ConstructionGrammar.Specificity : Type

How specified a construction's form side is ([Gol03]:220, Table 8).

Specificity	Example
lexicallySpecified	"veggie-wrap", "must-read"
partiallyOpen	"N-wrap", "a simple ⟨PAL⟩"
fullyAbstract	[N⁰ N⁰ N⁰], [N′ PAL⁰ N]

• lexicallySpecified : Specificity
• partiallyOpen : Specificity
• fullyAbstract : Specificity

@[implicit_reducible]

instance ConstructionGrammar.instReprSpecificity : Repr Specificity

Equations

• ConstructionGrammar.instReprSpecificity = { reprPrec := ConstructionGrammar.instReprSpecificity.repr }

def ConstructionGrammar.instReprSpecificity.repr : Specificity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqSpecificity : DecidableEq Specificity

Equations

• ConstructionGrammar.instDecidableEqSpecificity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive ConstructionGrammar.InheritanceMode : Type

Mode of information transfer in an inheritance link ([Gol95] §3.3.1, p. 73–74).

[Gol95] distinguishes two modes, orthogonal to link type:

• Normal: child inherits defaults from parent but may override them. Allows subregularities and exceptions. The only mode used in [Gol95]'s system.
• Complete: all information from dominating nodes is inherited strictly; no conflicts allowed. The mode "normally assumed in unification-based grammars" (p. 74, citing Kay 1984 and Fillmore & Kay 1993); the normal/complete distinction follows Flickinger, Pollard & Wasow (1985). Not exploited in [Gol95]'s constructional analysis.

Computational semantics for both modes: ConstructionGrammar.Inheritance.

• normal : InheritanceMode
• complete : InheritanceMode

@[implicit_reducible]

instance ConstructionGrammar.instReprInheritanceMode : Repr InheritanceMode

Equations

• ConstructionGrammar.instReprInheritanceMode = { reprPrec := ConstructionGrammar.instReprInheritanceMode.repr }

def ConstructionGrammar.instReprInheritanceMode.repr : InheritanceMode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqInheritanceMode : DecidableEq InheritanceMode

Equations

• ConstructionGrammar.instDecidableEqInheritanceMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive ConstructionGrammar.LinkType : Type

Type of semantic relation in an inheritance link ([Gol95] §3.3.2, p. 75).

[Gol95] distinguishes four major link types:

• I_P (Polysemy): relates the central sense of a construction to its extensions. Each extension inherits syntax but differs in meaning (e.g., the six senses of the ditransitive, pp. 75–77).
• I_M (Metaphorical extension): source and target related by systematic metaphor (e.g., caused-motion → resultative via the motion→change metaphor, p. 81).
• I_S (Subpart): one construction is a proper subpart of another (e.g., intransitive motion is a subpart of caused-motion, p. 78).
• I_I (Instance): one construction is a more fully specified version of another (e.g., drive-crazy is an instance of the resultative, p. 79).

• polysemy : LinkType
• metaphorical : LinkType
• subpart : LinkType
• instance : LinkType

def ConstructionGrammar.instReprLinkType.repr : LinkType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprLinkType : Repr LinkType

Equations

• ConstructionGrammar.instReprLinkType = { reprPrec := ConstructionGrammar.instReprLinkType.repr }

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqLinkType : DecidableEq LinkType

Equations

• ConstructionGrammar.instDecidableEqLinkType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive ConstructionGrammar.BarLevel : Type

X-bar level of a syntactic position or constructional output.

• zero : BarLevel
• bar : BarLevel
• phrase : BarLevel

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqBarLevel : DecidableEq BarLevel

Equations

• ConstructionGrammar.instDecidableEqBarLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ConstructionGrammar.instReprBarLevel.repr : BarLevel → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprBarLevel : Repr BarLevel

Equations

• ConstructionGrammar.instReprBarLevel = { reprPrec := ConstructionGrammar.instReprBarLevel.repr }

Typed slots

[Dun25] distinguishes three representation levels for slot content — LEX (a fixed lexeme), SYN (any word of a category), SEM+ (any expression meeting a semantic constraint) — and [KF99] add headed phrases, grammatical functions, coreference indices, and syntactic constraints. The phrasal filler (any phrase, no fixed head) is the filler type of phrasal compounds and PAL constructions.

inductive ConstructionGrammar.SlotFiller (Lex : Type u_1) : Type u_1

A slot's filler: the representation level of slot content.

Parameterized over Lex (the lexeme type) so the same representation works for strings, morphemes, or phonological forms.

• fixed {Lex : Type u_1} : Lex → SlotFiller Lex

  A specific word form (LEX level): fixed "must"

• open_ {Lex : Type u_1} : UD.UPOS → SlotFiller Lex

  Any word of a given POS category (SYN level): open_ .VERB

• headed {Lex : Type u_1} : Lex → UD.UPOS → SlotFiller Lex

  A phrase headed by a specific lexeme ([KF99]): headed "doing" .VERB is a VP headed by doing. LEX-level — the head lexeme is fixed even though the phrase is open.

• semantic {Lex : Type u_1} : String → SlotFiller Lex

  A semantically constrained slot ([Dun25], SEM+ level): semantic "animate" is any expression denoting an animate.

• phrasal {Lex : Type u_1} : SlotFiller Lex

  Any phrase, with no fixed head and no category restriction on its internal structure — the filler of a phrasal-compound or PAL slot (the ⟨phrase⟩ node of [GS25]'s Figure 5).

def ConstructionGrammar.instDecidableEqSlotFiller.decEq {Lex✝ : Type u_1} [DecidableEq Lex✝] (x✝ x✝¹ : SlotFiller Lex✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.fixed a) (ConstructionGrammar.SlotFiller.fixed b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.fixed a) (ConstructionGrammar.SlotFiller.open_ a_1) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.fixed a) (ConstructionGrammar.SlotFiller.headed a_1 a_2) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.fixed a) (ConstructionGrammar.SlotFiller.semantic a_1) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.fixed a) ConstructionGrammar.SlotFiller.phrasal = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.open_ a) (ConstructionGrammar.SlotFiller.fixed a_1) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.open_ a) (ConstructionGrammar.SlotFiller.open_ b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.open_ a) (ConstructionGrammar.SlotFiller.headed a_1 a_2) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.open_ a) (ConstructionGrammar.SlotFiller.semantic a_1) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.open_ a) ConstructionGrammar.SlotFiller.phrasal = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.headed a a_1) (ConstructionGrammar.SlotFiller.fixed a_2) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.headed a a_1) (ConstructionGrammar.SlotFiller.open_ a_2) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.headed a a_1) (ConstructionGrammar.SlotFiller.semantic a_2) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.headed a a_1) ConstructionGrammar.SlotFiller.phrasal = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.semantic a) (ConstructionGrammar.SlotFiller.fixed a_1) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.semantic a) (ConstructionGrammar.SlotFiller.open_ a_1) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.semantic a) (ConstructionGrammar.SlotFiller.headed a_1 a_2) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.semantic a) (ConstructionGrammar.SlotFiller.semantic b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq (ConstructionGrammar.SlotFiller.semantic a) ConstructionGrammar.SlotFiller.phrasal = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq ConstructionGrammar.SlotFiller.phrasal (ConstructionGrammar.SlotFiller.fixed a) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq ConstructionGrammar.SlotFiller.phrasal (ConstructionGrammar.SlotFiller.open_ a) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq ConstructionGrammar.SlotFiller.phrasal (ConstructionGrammar.SlotFiller.headed a a_1) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq ConstructionGrammar.SlotFiller.phrasal (ConstructionGrammar.SlotFiller.semantic a) = isFalse ⋯
• ConstructionGrammar.instDecidableEqSlotFiller.decEq ConstructionGrammar.SlotFiller.phrasal ConstructionGrammar.SlotFiller.phrasal = isTrue ⋯

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqSlotFiller {Lex✝ : Type u_1} [DecidableEq Lex✝] : DecidableEq (SlotFiller Lex✝)

Equations

• ConstructionGrammar.instDecidableEqSlotFiller = ConstructionGrammar.instDecidableEqSlotFiller.decEq

@[implicit_reducible]

instance ConstructionGrammar.instReprSlotFiller {Lex✝ : Type u_1} [Repr Lex✝] : Repr (SlotFiller Lex✝)

Equations

• ConstructionGrammar.instReprSlotFiller = { reprPrec := ConstructionGrammar.instReprSlotFiller.repr }

def ConstructionGrammar.instReprSlotFiller.repr {Lex✝ : Type u_1} [Repr Lex✝] : SlotFiller Lex✝ → ℕ → Std.Format

Equations

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

def ConstructionGrammar.SlotFiller.isOpen {Lex : Type u_1} : SlotFiller Lex → Bool

Is this slot open (not lexically anchored)?

open_ (SYN), semantic (SEM+), and phrasal slots count as open for abstraction-level computation. headed slots do not: they fix the head lexeme even though the phrase is open.

Equations

• (ConstructionGrammar.SlotFiller.fixed a).isOpen = false
• (ConstructionGrammar.SlotFiller.open_ a).isOpen = true
• (ConstructionGrammar.SlotFiller.headed a a_1).isOpen = false
• (ConstructionGrammar.SlotFiller.semantic a).isOpen = true
• ConstructionGrammar.SlotFiller.phrasal.isOpen = true

inductive ConstructionGrammar.GramFunction : Type

Grammatical function of a valence member ([KF99], Figure 12). Distinct from semantic role: a subject (gf) can be an agent, theme, or experiencer (role).

• subj : GramFunction
• comp : GramFunction
• obj : GramFunction
• pred : GramFunction

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqGramFunction : DecidableEq GramFunction

Equations

• ConstructionGrammar.instDecidableEqGramFunction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ConstructionGrammar.instReprGramFunction : Repr GramFunction

Equations

• ConstructionGrammar.instReprGramFunction = { reprPrec := ConstructionGrammar.instReprGramFunction.repr }

def ConstructionGrammar.instReprGramFunction.repr : GramFunction → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev ConstructionGrammar.RefIndex : Type

Referential index for cross-slot coreference constraints. Slots sharing a RefIndex have unified semantic values ([KF99]'s #1, #2).

Equations

• ConstructionGrammar.RefIndex = ℕ

inductive ConstructionGrammar.SlotConstraint : Type

Syntactic constraint on a slot ([KF99], Figure 12).

• locMinus : SlotConstraint
• negMinus : SlotConstraint
• refEmpty : SlotConstraint

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqSlotConstraint : DecidableEq SlotConstraint

Equations

• ConstructionGrammar.instDecidableEqSlotConstraint x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ConstructionGrammar.instReprSlotConstraint.repr : SlotConstraint → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprSlotConstraint : Repr SlotConstraint

Equations

• ConstructionGrammar.instReprSlotConstraint = { reprPrec := ConstructionGrammar.instReprSlotConstraint.repr }

structure ConstructionGrammar.Slot (Lex : Type u_1) : Type u_1

A slot in a construction's form: filler content, semantic role, headedness, and the bar level of the position itself. Fixed slots (like "let" in let alone) have role := none since they carry no independent semantic role. level := none leaves the position's bar level unspecified.

• filler : SlotFiller Lex

  What fills this slot

• role : Option String

  Semantic role label (agent, theme, etc.), if any

• isHead : Bool

  Whether this slot is the head of the construction

• level : Option BarLevel

  Bar level of the position (some .zero = a word-level slot)

• gf : Option GramFunction

  Grammatical function (subj, comp, obj, pred) — [KF99]

• refIdx : Option RefIndex

  Coreference index: slots sharing an index have unified semantics

• constraints : List SlotConstraint

  Syntactic constraints on this slot ([loc -], [neg -], [ref ∅])

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqSlot {Lex✝ : Type u_1} [DecidableEq Lex✝] : DecidableEq (Slot Lex✝)

Equations

• ConstructionGrammar.instDecidableEqSlot = ConstructionGrammar.instDecidableEqSlot.decEq

def ConstructionGrammar.instDecidableEqSlot.decEq {Lex✝ : Type u_1} [DecidableEq Lex✝] (x✝ x✝¹ : Slot Lex✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprSlot {Lex✝ : Type u_1} [Repr Lex✝] : Repr (Slot Lex✝)

Equations

• ConstructionGrammar.instReprSlot = { reprPrec := ConstructionGrammar.instReprSlot.repr }

def ConstructionGrammar.instReprSlot.repr {Lex✝ : Type u_1} [Repr Lex✝] : Slot Lex✝ → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev ConstructionGrammar.TypedForm (Lex : Type u_1) : Type u_1

A typed form: the form side of a construction as a sequence of slots.

Equations

• ConstructionGrammar.TypedForm Lex = List (ConstructionGrammar.Slot Lex)

def ConstructionGrammar.Slot.IsPhraseInWordSlot {Lex : Type u_1} (s : Slot Lex) : Prop

A phrase in a word-level slot: phrasal filler, zero-level position. The defining configuration of phrasal compounds and the PAL construction ([GS25]) — and the cell lexical-integrity hypotheses rule out.

Equations

• s.IsPhraseInWordSlot = (s.filler = ConstructionGrammar.SlotFiller.phrasal ∧ s.level = some ConstructionGrammar.BarLevel.zero)

@[implicit_reducible]

instance ConstructionGrammar.instDecidableIsPhraseInWordSlotOfDecidableEq {Lex : Type u_1} [DecidableEq Lex] (s : Slot Lex) : Decidable s.IsPhraseInWordSlot

Equations

• ConstructionGrammar.instDecidableIsPhraseInWordSlotOfDecidableEq s = ConstructionGrammar.instDecidableIsPhraseInWordSlotOfDecidableEq._aux_1 s

Abstraction level and derived specificity

def ConstructionGrammar.abstractionLevel {Lex : Type u_1} (form : TypedForm Lex) : ℚ

Proportion of open slots: a continuous [0,1] measure of abstraction.

[Dun25] defines four discrete abstraction orders based on which representation levels appear; this computes the continuous proportion underlying those orders, and derivedSpecificity maps to the three-way Specificity enum.

Equations

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

def ConstructionGrammar.derivedSpecificity {Lex : Type u_1} (form : TypedForm Lex) : Specificity

Derive Specificity from the slot structure.

Condition	Result
All slots open	.fullyAbstract
No slots open	.lexicallySpecified
Mix of fixed and open	.partiallyOpen

Changing a slot from open to fixed automatically changes the specificity.

Equations

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

def ConstructionGrammar.hasConstraint {Lex : Type u_1} (form : TypedForm Lex) (c : SlotConstraint) : Bool

Does any slot in the form bear a given constraint?

Equations

• ConstructionGrammar.hasConstraint form c = List.any form fun (x : ConstructionGrammar.Slot Lex) => x.constraints.any fun (x : ConstructionGrammar.SlotConstraint) => x == c

def ConstructionGrammar.refGroupCount {Lex : Type u_1} (form : TypedForm Lex) : ℕ

Count of distinct coreference groups in a form.

Equations

• ConstructionGrammar.refGroupCount form = (List.filterMap (fun (x : ConstructionGrammar.Slot Lex) => x.refIdx) form).dedup.length

Characterization lemmas

@[simp]

theorem ConstructionGrammar.abstractionLevel_nil {Lex : Type u_1} : abstractionLevel [] = 0

theorem ConstructionGrammar.abstractionLevel_nonneg {Lex : Type u_1} (form : TypedForm Lex) : 0 ≤ abstractionLevel form

theorem ConstructionGrammar.abstractionLevel_le_one {Lex : Type u_1} (form : TypedForm Lex) : abstractionLevel form ≤ 1

theorem ConstructionGrammar.derivedSpecificity_eq_fullyAbstract_iff {Lex : Type u_1} (form : TypedForm Lex) : derivedSpecificity form = Specificity.fullyAbstract ↔ ∀ s ∈ form, s.filler.isOpen = true

A form is fully abstract exactly when every slot is open (vacuously so for the empty form).

theorem ConstructionGrammar.derivedSpecificity_eq_lexicallySpecified_iff {Lex : Type u_1} (form : TypedForm Lex) : derivedSpecificity form = Specificity.lexicallySpecified ↔ form ≠ [] ∧ ∀ s ∈ form, s.filler.isOpen = false

A form is lexically specified exactly when it is nonempty and no slot is open.

Constructions and the network

structure ConstructionGrammar.Construction : Type

A construction: a learned pairing of form and function. The form is a TypedForm; name is a display label; specificity is derived from the form (Construction.specificity), not stipulated.

• name : String
• form : TypedForm String
• meaning : String
• pragmaticFunction : Option String

def ConstructionGrammar.instDecidableEqConstruction.decEq (x✝ x✝¹ : Construction) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqConstruction : DecidableEq Construction

Equations

• ConstructionGrammar.instDecidableEqConstruction = ConstructionGrammar.instDecidableEqConstruction.decEq

def ConstructionGrammar.instReprConstruction.repr : Construction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprConstruction : Repr Construction

Equations

• ConstructionGrammar.instReprConstruction = { reprPrec := ConstructionGrammar.instReprConstruction.repr }

def ConstructionGrammar.Construction.specificity (c : Construction) : Specificity

A construction's specificity, derived from its slot structure.

Equations

• c.specificity = ConstructionGrammar.derivedSpecificity c.form

structure ConstructionGrammar.InheritanceLink : Type

An inheritance link between two constructions in the network.

Each link specifies both how information flows (mode, §3.3.1) and what semantic relation holds (linkType, §3.3.2). Links without a specific semantic relation (e.g., general taxonomic inheritance of shared morphophonological properties) use linkType := none.

• parent : String
• child : String
• mode : InheritanceMode
• linkType : Option LinkType
• sharedProperties : List String
• overriddenProperties : List String

@[implicit_reducible]

instance ConstructionGrammar.instReprInheritanceLink : Repr InheritanceLink

Equations

• ConstructionGrammar.instReprInheritanceLink = { reprPrec := ConstructionGrammar.instReprInheritanceLink.repr }

def ConstructionGrammar.instReprInheritanceLink.repr : InheritanceLink → ℕ → Std.Format

Equations

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

def ConstructionGrammar.instDecidableEqInheritanceLink.decEq (x✝ x✝¹ : InheritanceLink) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instDecidableEqInheritanceLink : DecidableEq InheritanceLink

Equations

• ConstructionGrammar.instDecidableEqInheritanceLink = ConstructionGrammar.instDecidableEqInheritanceLink.decEq

structure ConstructionGrammar.Constructicon : Type

A constructicon: a network of constructions connected by inheritance links.

• constructions : List Construction
• links : List InheritanceLink

def ConstructionGrammar.instReprConstructicon.repr : Constructicon → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.instReprConstructicon : Repr Constructicon

Equations

• ConstructionGrammar.instReprConstructicon = { reprPrec := ConstructionGrammar.instReprConstructicon.repr }