Constructions and the constructicon

A construction is a learned pairing of a form and a meaning ([Gol06]), the basic unit of grammatical knowledge in CxG. The form side is a TypedForm: a sequence of Slots, each fixing a lexeme, opening a category, or admitting any phrase, with a construction's Specificity derived from its slot structure rather than stipulated.

Main definitions

• SlotFiller, Slot, TypedForm: the typed form side
• derivedSpecificity, HasConstraint, refGroupCount: measures derived from forms
• Construction, Construction.specificity, Construction.map: typed form–meaning pairings
• InheritanceLink, Constructicon: the network

inductive ConstructionGrammar.Specificity : Type

How specified a construction's form side is: [Gol03]'s degree-of-abstraction continuum, discretized as in [GS25]'s Table 8.

• lexicallySpecified : Specificity

  Every slot lexically filled: veggie-wrap, must-read.

• partiallyOpen : Specificity

  Fixed and open slots mixed: N-wrap, a simple ⟨PAL⟩.

• fullyAbstract : Specificity

  Every slot open: [N⁰ N⁰ N⁰], [N′ PAL⁰ N].

@[instance_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.

@[instance_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, orthogonal to the link's semantic relation ([Gol95] §3.3.1, p. 73–74).

• normal : InheritanceMode

  The child inherits defaults from its parents but may override them — the only mode [Gol95] uses.

• complete : InheritanceMode

  All information is inherited strictly, with no conflicts allowed — the mode "normally assumed in unification-based grammars" (p. 74).

@[instance_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.

@[instance_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

The semantic relation an inheritance link records: [Gol95]'s four major link types (§3.3.2, p. 75).

• polysemy : LinkType

  I_P: relates a construction's central sense to an extension, which inherits the syntax but differs in meaning (the six senses of the ditransitive, pp. 75–77).

• metaphorical : LinkType

  I_M: source and target related by a systematic metaphor (caused-motion → resultative via motion→change, p. 81).

• subpart : LinkType

  I_S: the child is a proper subpart of the parent (intransitive motion inside caused-motion, p. 78).

• instance : LinkType

  I_I: the child is a more fully specified version of the parent (drive-crazy as an instance of the resultative, p. 79).

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

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprLinkType : Repr LinkType

Equations

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

@[instance_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

  X⁰, a word-level position.

• bar : BarLevel

  X′, an intermediate projection.

• phrase : BarLevel

  XP, a full phrase.

@[instance_reducible]

instance ConstructionGrammar.instDecidableEqBarLevel : DecidableEq BarLevel

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprBarLevel : Repr BarLevel

Equations

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

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

Equations

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

Typed slots

Slot content comes at [Dun25]'s three representation levels — LEX (a fixed lexeme), SYN (any word of a category), SEM (a semantic constraint) — plus [KF99]'s headed phrases, grammatical functions, coreference indices, and slot constraints.

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 ⋯

@[instance_reducible]

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

Equations

• ConstructionGrammar.instDecidableEqSlotFiller = ConstructionGrammar.instDecidableEqSlotFiller.decEq

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.

@[instance_reducible]

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

Equations

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

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

Whether a slot is open — not lexically anchored: open_, semantic, and phrasal fillers count as open; fixed and headed do not, the latter fixing its 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 can be an agent, a theme, or an experiencer.

• subj : GramFunction

  Subject.

• comp : GramFunction

  Clausal or verbal complement.

• obj : GramFunction

  Direct object.

• pred : GramFunction

  Predicative complement or secondary predicate.

@[instance_reducible]

instance ConstructionGrammar.instDecidableEqGramFunction : DecidableEq GramFunction

Equations

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

@[instance_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

  [loc -]: must occur left-isolated, not VP-internal.

• negMinus : SlotConstraint

  [neg -]: cannot be negated.

• refEmpty : SlotConstraint

  [ref ∅]: nonreferential — no variable-binding function.

@[instance_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.

@[instance_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, headedness, and the bar level of the position itself. level := none leaves the position's bar level unspecified; slots sharing a refIdx are co-indexed, the hook by which a typed meaning pole refers to slots.

• filler : SlotFiller Lex

  What fills this slot

• 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 ∅])

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.

@[instance_reducible]

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

Equations

• ConstructionGrammar.instDecidableEqSlot = ConstructionGrammar.instDecidableEqSlot.decEq

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.

@[instance_reducible]

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

Equations

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

@[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 that lexical-integrity hypotheses rule out.

Equations

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

@[instance_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

Derived specificity

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

The specificity of a form: fullyAbstract when every slot is open (vacuously so for the empty form), lexicallySpecified when none is, and partiallyOpen otherwise.

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) : Prop

Some slot in the form bears the constraint c.

Equations

• ConstructionGrammar.HasConstraint form c = ∃ s ∈ form, c ∈ s.constraints

@[instance_reducible]

instance ConstructionGrammar.instDecidableHasConstraint {Lex : Type u_1} (form : TypedForm Lex) (c : SlotConstraint) : Decidable (HasConstraint form c)

Equations

• ConstructionGrammar.instDecidableHasConstraint form c = ConstructionGrammar.instDecidableHasConstraint._aux_1 form 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

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 (Sem : Type u_1) : Type u_1

A construction: a learned pairing of form and meaning. The meaning pole is typed by the domain that owns the construction — a composition rule, a MeaningComponents contribution, a presupposition — with Unit for a purely formal record or a defective, form-only construction.

• name : String
• form : TypedForm String
• meaning : Sem

  The meaning pole.

• pragmaticPoint : Bool

  Whether the construction carries a conventional pragmatic point ([FKOC88] §1.1.4).

@[instance_reducible]

instance ConstructionGrammar.instDecidableEqConstruction {Sem✝ : Type u_1} [DecidableEq Sem✝] : DecidableEq (Construction Sem✝)

Equations

• ConstructionGrammar.instDecidableEqConstruction = ConstructionGrammar.instDecidableEqConstruction.decEq

def ConstructionGrammar.instDecidableEqConstruction.decEq {Sem✝ : Type u_1} [DecidableEq Sem✝] (x✝ x✝¹ : Construction Sem✝) : Decidable (x✝ = x✝¹)

Equations

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

def ConstructionGrammar.instReprConstruction.repr {Sem✝ : Type u_1} [Repr Sem✝] : Construction Sem✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprConstruction {Sem✝ : Type u_1} [Repr Sem✝] : Repr (Construction Sem✝)

Equations

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

def ConstructionGrammar.Construction.specificity {Sem : Type u_1} (c : Construction Sem) : Specificity

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

Equations

• c.specificity = ConstructionGrammar.derivedSpecificity c.form

def ConstructionGrammar.Construction.map {Sem : Type u_1} {Sem' : Type u_2} (f : Sem → Sem') (c : Construction Sem) : Construction Sem'

Reinterpret the meaning pole along f, keeping the form.

Equations

• ConstructionGrammar.Construction.map f c = { name := c.name, form := c.form, meaning := f c.meaning, pragmaticPoint := c.pragmaticPoint }

structure ConstructionGrammar.InheritanceLink : Type

An inheritance link between two constructions in the network, recording how information flows and what semantic relation holds; purely taxonomic links use linkType := none.

• parent : String

  Name of the parent construction.

• child : String

  Name of the child construction.

• mode : InheritanceMode

  How information flows along the link.

• linkType : Option LinkType

  The semantic relation the link records, if any.

• sharedProperties : List String

  Properties the child inherits from the parent.

• overriddenProperties : List String

  Inherited properties the child overrides.

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

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprInheritanceLink : Repr InheritanceLink

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instDecidableEqInheritanceLink : DecidableEq InheritanceLink

Equations

• ConstructionGrammar.instDecidableEqInheritanceLink = ConstructionGrammar.instDecidableEqInheritanceLink.decEq

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

Equations

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

structure ConstructionGrammar.Constructicon (Sem : Type u_2) : Type u_2

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

• constructions : List (Construction Sem)

  The inventory of constructions.

• links : List InheritanceLink

  The inheritance links, keyed by construction name.

def ConstructionGrammar.instReprConstructicon.repr {Sem✝ : Type u_2} [Repr Sem✝] : Constructicon Sem✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ConstructionGrammar.instReprConstructicon {Sem✝ : Type u_2} [Repr Sem✝] : Repr (Constructicon Sem✝)

Equations

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