Coordination: morphosyntactic typology

[Has07] [Sta00] [MS16] [DH13a] [DH13b]

Per-language typological substrate for coordination across three frameworks:

1. [Has07] structural typology: syndesis (asyndetic / monosyndetic / bisyndetic), coordinator position, structural patterns, and diachronic source (comitative vs additive focus particle).
2. [Sta00] AND/WITH typology: derived from WALS Ch 63 (lexical identity of "and" and "with").
3. WALS Ch 56/63/64: conjunction-quantifier relation, NP conjunction, nominal-vs-verbal conjunction.

Mirrors the Linglib/Typology/{Possession,Negation,Question,Comparison}.lean substrate-extension pattern. Fragment-importable; cross-linguistic theorems live in Studies/Haspelmath2007.lean (structural typology + 19-language sample), Studies/MitrovicSauerland2016.lean (J/MU framework + M&S generalisations), and Studies/Stassen2000.lean (AND/WITH typology + 15- language WALS sample).

Main declarations

• Syndesis, CoordinatorPosition, CoordPattern, DiachronicSource — Haspelmath structural enums.
• AndWithStatus — Stassen 2000 binary classification.
• ConjQuantRelation, ConjComitativeRelation, NomVerbalConjRelation — WALS Ch 56/63/64 aliases.
• SourcedEntry, ConjunctionSystem — per-language structs.
• CoordinationProfile — WALS profile bundle.
• ConjunctionSystem.hasStrategy, muIsAdditive, hasSource, hasMonosyndetic, hasBisyndetic, muBoundness — Prop-valued decidable predicates.

Implementation notes

• Helper predicates are Prop with explicit Decidable instances rather than Bool-returning, so consumers can write sys.hasStrategy s directly in theorem statements without = true boilerplate while retaining decide-checkability over finite samples.
• DiachronicSource collapses Heine's full grammaticalization-source taxonomy to two main pathways relevant for coordination (comitative, focus particle); other pathways are conflated under .other.
• AndWithStatus is [Sta00]'s binary classification; some authors (e.g. Mauri 2008) argue for a finer multi-way split.

[MS14] conjunction strategy

inductive Syntax.Coordination.ConjunctionStrategy : Type

Cross-linguistic conjunction strategy. [MS14] decompose DP conjunction into three semantic pieces: J (set intersection), MU (subset), and a type-shifter; languages vary in which pieces are overtly realized.

• jOnly : ConjunctionStrategy

  Only J particle overt (e.g., English "and", Hungarian "es", Georgian "da").

• muOnly : ConjunctionStrategy

  Only MU particles overt (e.g., Japanese "mo...mo", Hungarian "is...is", Georgian "-c...-c").

• jMu : ConjunctionStrategy

  Both J and MU overt (e.g., Hungarian "is es...is", Georgian "-c da...-c").

@[implicit_reducible]

instance Syntax.Coordination.instDecidableEqConjunctionStrategy : DecidableEq ConjunctionStrategy

Equations

• Syntax.Coordination.instDecidableEqConjunctionStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Syntax.Coordination.instReprConjunctionStrategy.repr : ConjunctionStrategy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Coordination.instReprConjunctionStrategy : Repr ConjunctionStrategy

Equations

• Syntax.Coordination.instReprConjunctionStrategy = { reprPrec := Syntax.Coordination.instReprConjunctionStrategy.repr }

def Syntax.Coordination.ConjunctionStrategy.overtMorphemeCount : ConjunctionStrategy → ℕ

Number of overt functional morphemes per strategy. Under [MS16] the underlying structure always has 3 pieces (J + MU1 + MU2); what varies is how many are pronounced.

Equations

• Syntax.Coordination.ConjunctionStrategy.jOnly.overtMorphemeCount = 1
• Syntax.Coordination.ConjunctionStrategy.muOnly.overtMorphemeCount = 2
• Syntax.Coordination.ConjunctionStrategy.jMu.overtMorphemeCount = 3

def Syntax.Coordination.ConjunctionStrategy.semanticPieceCount : ℕ

Under [MS16] there are always 3 semantic pieces.

Equations

• Syntax.Coordination.ConjunctionStrategy.semanticPieceCount = 3

def Syntax.Coordination.ConjunctionStrategy.predictedTransparency : ConjunctionStrategy → ℕ

[MS16] + Transparency Principle: more overt morphemes -> easier to acquire (closer to a 1-to-1 form-meaning mapping).

Equations

• Syntax.Coordination.ConjunctionStrategy.predictedTransparency = Syntax.Coordination.ConjunctionStrategy.overtMorphemeCount

Haspelmath 2007 structural enums

inductive Syntax.Coordination.Syndesis : Type

Syndesis: presence and number of overt coordinators ([Has07] §1).

• asyndetic : Syndesis

  A B (juxtaposition, no overt linker).

• monosyndetic : Syndesis

  A co-B (single coordinator).

• bisyndetic : Syndesis

  co-A co-B (two coordinators, one per coordinand).

@[implicit_reducible]

instance Syntax.Coordination.instDecidableEqSyndesis : DecidableEq Syndesis

Equations

• Syntax.Coordination.instDecidableEqSyndesis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Syntax.Coordination.instBEqSyndesis.beq : Syndesis → Syndesis → Bool

Equations

• Syntax.Coordination.instBEqSyndesis.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Syntax.Coordination.instBEqSyndesis : BEq Syndesis

Equations

• Syntax.Coordination.instBEqSyndesis = { beq := Syntax.Coordination.instBEqSyndesis.beq }

@[implicit_reducible]

instance Syntax.Coordination.instReprSyndesis : Repr Syndesis

Equations

• Syntax.Coordination.instReprSyndesis = { reprPrec := Syntax.Coordination.instReprSyndesis.repr }

def Syntax.Coordination.instReprSyndesis.repr : Syndesis → ℕ → Std.Format

Equations

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

inductive Syntax.Coordination.CoordinatorPosition : Type

Coordinator position relative to its coordinand ([Has07] §1.2).

[Has07] notes that co-A B (prepositive on first coordinand only) is unattested (cf. [Sta00], n=260).

• prepositive : CoordinatorPosition

  co precedes coordinand: "and A" / English "both X".

• postpositive : CoordinatorPosition

  co follows coordinand: "A-and" / Latin "X-que".

@[implicit_reducible]

instance Syntax.Coordination.instDecidableEqCoordinatorPosition : DecidableEq CoordinatorPosition

Equations

• Syntax.Coordination.instDecidableEqCoordinatorPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Syntax.Coordination.instBEqCoordinatorPosition : BEq CoordinatorPosition

Equations

• Syntax.Coordination.instBEqCoordinatorPosition = { beq := Syntax.Coordination.instBEqCoordinatorPosition.beq }

def Syntax.Coordination.instBEqCoordinatorPosition.beq : CoordinatorPosition → CoordinatorPosition → Bool

Equations

• Syntax.Coordination.instBEqCoordinatorPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Syntax.Coordination.instReprCoordinatorPosition : Repr CoordinatorPosition

Equations

• Syntax.Coordination.instReprCoordinatorPosition = { reprPrec := Syntax.Coordination.instReprCoordinatorPosition.repr }

def Syntax.Coordination.instReprCoordinatorPosition.repr : CoordinatorPosition → ℕ → Std.Format

Equations

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

inductive Syntax.Coordination.CoordPattern : Type

Structural pattern for binary coordination ([Has07] (17)).

Monosyndetic: 3 attested patterns (of 4 logically possible). The fourth monosyndetic pattern co-A B (prepositive on first coordinand only) is unattested per [Sta00], n=260; the absence is encoded as a theorem rather than by omission (see Studies/Haspelmath2007.lean).

Bisyndetic: 4 attested patterns.

• a_co_b : CoordPattern

  A co-B: medial prepositive (English "A and B").

• a'co_b : CoordPattern

  A-co B: medial postpositive on 1st (Tibetan "A-daŋ B").

• a_b'co : CoordPattern

  A B-co: final postpositive (Latin "senatus populus-que").

• co'a_b : CoordPattern

  co-A B: prepositive on first coordinand only — typologically unattested for conjunction ([Sta00], n=260).

• co'a_co'b : CoordPattern

  co-A co-B: prepositive bisyndetic (Yoruba "àtí A àtí B").

• a'co_b'co : CoordPattern

  A-co B-co: postpositive bisyndetic (Martuthunira "A-thurti B-thurti").

• a'co_co'b : CoordPattern

  A-co co-B: mixed bisyndetic (Homeric Greek "A-te kaì B").

• co'a_b'co : CoordPattern

  co-A B-co: mixed bisyndetic (Latin "et A B-que").

@[implicit_reducible]

instance Syntax.Coordination.instDecidableEqCoordPattern : DecidableEq CoordPattern

Equations

• Syntax.Coordination.instDecidableEqCoordPattern x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Syntax.Coordination.instBEqCoordPattern : BEq CoordPattern

Equations

• Syntax.Coordination.instBEqCoordPattern = { beq := Syntax.Coordination.instBEqCoordPattern.beq }

def Syntax.Coordination.instBEqCoordPattern.beq : CoordPattern → CoordPattern → Bool

Equations

• Syntax.Coordination.instBEqCoordPattern.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Syntax.Coordination.instReprCoordPattern.repr : CoordPattern → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Coordination.instReprCoordPattern : Repr CoordPattern

Equations

• Syntax.Coordination.instReprCoordPattern = { reprPrec := Syntax.Coordination.instReprCoordPattern.repr }

def Syntax.Coordination.CoordPattern.syndesis : CoordPattern → Syndesis

Classify a pattern's syndesis.

Equations

• Syntax.Coordination.CoordPattern.a_co_b.syndesis = Syntax.Coordination.Syndesis.monosyndetic
• Syntax.Coordination.CoordPattern.a'co_b.syndesis = Syntax.Coordination.Syndesis.monosyndetic
• Syntax.Coordination.CoordPattern.a_b'co.syndesis = Syntax.Coordination.Syndesis.monosyndetic
• Syntax.Coordination.CoordPattern.co'a_b.syndesis = Syntax.Coordination.Syndesis.monosyndetic
• Syntax.Coordination.CoordPattern.co'a_co'b.syndesis = Syntax.Coordination.Syndesis.bisyndetic
• Syntax.Coordination.CoordPattern.a'co_b'co.syndesis = Syntax.Coordination.Syndesis.bisyndetic
• Syntax.Coordination.CoordPattern.a'co_co'b.syndesis = Syntax.Coordination.Syndesis.bisyndetic
• Syntax.Coordination.CoordPattern.co'a_b'co.syndesis = Syntax.Coordination.Syndesis.bisyndetic

inductive Syntax.Coordination.DiachronicSource : Type

Diachronic source of conjunction constructions ([Has07] §5.1).

• comitative : DiachronicSource

  "with" → coordinator (gives A co-B or A-co B).

• focusParticle : DiachronicSource

  "also/too" → coordinator (gives A-co B-co).

• other : DiachronicSource

  Other or unknown source.

@[implicit_reducible]

instance Syntax.Coordination.instDecidableEqDiachronicSource : DecidableEq DiachronicSource

Equations

• Syntax.Coordination.instDecidableEqDiachronicSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Syntax.Coordination.instBEqDiachronicSource.beq : DiachronicSource → DiachronicSource → Bool

Equations

• Syntax.Coordination.instBEqDiachronicSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Syntax.Coordination.instBEqDiachronicSource : BEq DiachronicSource

Equations

• Syntax.Coordination.instBEqDiachronicSource = { beq := Syntax.Coordination.instBEqDiachronicSource.beq }

def Syntax.Coordination.instReprDiachronicSource.repr : DiachronicSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Coordination.instReprDiachronicSource : Repr DiachronicSource

Equations

• Syntax.Coordination.instReprDiachronicSource = { reprPrec := Syntax.Coordination.instReprDiachronicSource.repr }

def Syntax.Coordination.DiachronicSource.expectedSyndesis : DiachronicSource → Option Syndesis

Haspelmath's link between diachronic source and structural syndesis. Returns the syndesis pattern expected from the source pathway; none for .other since we make no prediction there.

Equations

• Syntax.Coordination.DiachronicSource.comitative.expectedSyndesis = some Syntax.Coordination.Syndesis.monosyndetic
• Syntax.Coordination.DiachronicSource.focusParticle.expectedSyndesis = some Syntax.Coordination.Syndesis.bisyndetic
• Syntax.Coordination.DiachronicSource.other.expectedSyndesis = none

Stassen 2000 AND/WITH classification

inductive Syntax.Coordination.AndWithStatus : Type

[Sta00] AND/WITH classification of languages. AND-languages have structurally distinct coordinate and comitative strategies. WITH-languages use comitative encoding as the only strategy for NP conjunction (lexical identity of "and" and "with").

• andLang : AndWithStatus

  Coordinate and comitative are structurally distinct.

• withLang : AndWithStatus

  Comitative marker = coordinator.

@[implicit_reducible]

instance Syntax.Coordination.instDecidableEqAndWithStatus : DecidableEq AndWithStatus

Equations

• Syntax.Coordination.instDecidableEqAndWithStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Syntax.Coordination.instBEqAndWithStatus : BEq AndWithStatus

Equations

• Syntax.Coordination.instBEqAndWithStatus = { beq := Syntax.Coordination.instBEqAndWithStatus.beq }

def Syntax.Coordination.instBEqAndWithStatus.beq : AndWithStatus → AndWithStatus → Bool

Equations

• Syntax.Coordination.instBEqAndWithStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Syntax.Coordination.instReprAndWithStatus : Repr AndWithStatus

Equations

• Syntax.Coordination.instReprAndWithStatus = { reprPrec := Syntax.Coordination.instReprAndWithStatus.repr }

def Syntax.Coordination.instReprAndWithStatus.repr : AndWithStatus → ℕ → Std.Format

Equations

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

WALS aliases (Chs 56/63/64)

@[reducible, inline]

abbrev Syntax.Coordination.ConjQuantRelation : Type

WALS Ch 56: conjunction-quantifier relation.

Equations

• Syntax.Coordination.ConjQuantRelation = Data.WALS.F56A.ConjunctionsAndUniversalQuantifiers

@[reducible, inline]

abbrev Syntax.Coordination.ConjComitativeRelation : Type

WALS Ch 63: noun-phrase conjunction (and-vs-with).

Equations

• Syntax.Coordination.ConjComitativeRelation = Data.WALS.F63A.NounPhraseConjunction

@[reducible, inline]

abbrev Syntax.Coordination.NomVerbalConjRelation : Type

WALS Ch 64: nominal-vs-verbal conjunction.

Equations

• Syntax.Coordination.NomVerbalConjRelation = Data.WALS.F64A.NominalAndVerbalConjunction

def Syntax.Coordination.ConjComitativeRelation.toAndWithStatus : ConjComitativeRelation → AndWithStatus

Derive AND/WITH status from the conjunction-comitative relation ([Sta00]'s diagnostic).

Equations

• Syntax.Coordination.ConjComitativeRelation.toAndWithStatus Data.WALS.F63A.NounPhraseConjunction.andDifferentFromWith = Syntax.Coordination.AndWithStatus.andLang
• Syntax.Coordination.ConjComitativeRelation.toAndWithStatus Data.WALS.F63A.NounPhraseConjunction.andIdenticalToWith = Syntax.Coordination.AndWithStatus.withLang

Per-language structs

structure Syntax.Coordination.SourcedEntry : Type

A coordination entry annotated with its diachronic source. Wraps Coordinator (from Semantics/Coordination/Defs) with typological metadata. For languages with Fragment files, entry references the Fragment entry directly — no data duplication.

• entry : Coordinator

  The coordination morpheme entry.

• source : Option DiachronicSource

  Likely diachronic source, if known.

def Syntax.Coordination.instReprSourcedEntry.repr : SourcedEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Coordination.instReprSourcedEntry : Repr SourcedEntry

Equations

• Syntax.Coordination.instReprSourcedEntry = { reprPrec := Syntax.Coordination.instReprSourcedEntry.repr }

structure Syntax.Coordination.ConjunctionSystem : Type

A language's conjunction system (M&S framework).

• language : String

  Language name.

• morphemes : List SourcedEntry

  Available conjunction morphemes (sourced entries).

• strategies : List ConjunctionStrategy

  Which conjunction strategies are available (M&S classification).

• patterns : List CoordPattern

  Structural patterns attested ([Has07] classification).

• iso : String

  ISO 639-3 code.

@[implicit_reducible]

instance Syntax.Coordination.instReprConjunctionSystem : Repr ConjunctionSystem

Equations

• Syntax.Coordination.instReprConjunctionSystem = { reprPrec := Syntax.Coordination.instReprConjunctionSystem.repr }

def Syntax.Coordination.instReprConjunctionSystem.repr : ConjunctionSystem → ℕ → Std.Format

Equations

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

structure Syntax.Coordination.CoordinationProfile : Type

A language's coordination typology profile across WALS Chs 56, 63, 64.

• language : String

  Language name.

• iso : String

  ISO 639-3 code.

• family : String

  Language family.

• conjQuant : Option ConjQuantRelation

  Ch 56: conjunction-vs-universal-quantifier.

• conjComitative : Option ConjComitativeRelation

  Ch 63: "and" vs "with".

• nomVerbalConj : Option NomVerbalConjRelation

  Ch 64: NP-vs-VP conjunction.

• walsNotes : String

  Free-form provenance notes.

@[implicit_reducible]

instance Syntax.Coordination.instReprCoordinationProfile : Repr CoordinationProfile

Equations

• Syntax.Coordination.instReprCoordinationProfile = { reprPrec := Syntax.Coordination.instReprCoordinationProfile.repr }

def Syntax.Coordination.instReprCoordinationProfile.repr : CoordinationProfile → ℕ → Std.Format

Equations

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

def Syntax.Coordination.CoordinationProfile.andWithStatus (p : CoordinationProfile) : Option AndWithStatus

Derive AND/WITH status for a coordination profile from its Ch 63 value.

Equations

• p.andWithStatus = Option.map (fun (x : Syntax.Coordination.ConjComitativeRelation) => x.toAndWithStatus) p.conjComitative

Helper predicates

The five ConjunctionSystem.has* predicates and muIsAdditive are Prop-valued for clean theorem statements (no = true boilerplate). Each has an explicit Decidable instance so concrete checks over finite language samples close by decide.

def Syntax.Coordination.ConjunctionSystem.hasStrategy (sys : ConjunctionSystem) (s : ConjunctionStrategy) : Prop

Does a language make a given conjunction strategy available?

Equations

• sys.hasStrategy s = (s ∈ sys.strategies)

@[implicit_reducible]

instance Syntax.Coordination.instDecidableHasStrategy (sys : ConjunctionSystem) (s : ConjunctionStrategy) : Decidable (sys.hasStrategy s)

Equations

• Syntax.Coordination.instDecidableHasStrategy sys s = id inferInstance

def Syntax.Coordination.ConjunctionSystem.muIsAdditive (sys : ConjunctionSystem) : Prop

Does a language have a MU morpheme that also serves as the additive ("also/too") particle? Existential: at least one MU morpheme in the language's inventory has alsoAdditive = true.

Equations

• sys.muIsAdditive = ∃ (m : Syntax.Coordination.SourcedEntry), m ∈ sys.morphemes ∧ m.entry.role = Coordinator.Role.mu ∧ m.entry.alsoAdditive = true

@[implicit_reducible]

instance Syntax.Coordination.instDecidableMuIsAdditive (sys : ConjunctionSystem) : Decidable sys.muIsAdditive

Equations

• Syntax.Coordination.instDecidableMuIsAdditive sys = id inferInstance

def Syntax.Coordination.ConjunctionSystem.hasSource (sys : ConjunctionSystem) (s : DiachronicSource) : Prop

Does the language attest a morpheme with the given diachronic source?

Equations

• sys.hasSource s = ∃ (m : Syntax.Coordination.SourcedEntry), m ∈ sys.morphemes ∧ m.source = some s

@[implicit_reducible]

instance Syntax.Coordination.instDecidableHasSource (sys : ConjunctionSystem) (s : DiachronicSource) : Decidable (sys.hasSource s)

Equations

• Syntax.Coordination.instDecidableHasSource sys s = id inferInstance

def Syntax.Coordination.ConjunctionSystem.hasMonosyndetic (sys : ConjunctionSystem) : Prop

Does a language attest at least one monosyndetic pattern?

Equations

• sys.hasMonosyndetic = ∃ (p : Syntax.Coordination.CoordPattern), p ∈ sys.patterns ∧ p.syndesis = Syntax.Coordination.Syndesis.monosyndetic

@[implicit_reducible]

instance Syntax.Coordination.instDecidableHasMonosyndetic (sys : ConjunctionSystem) : Decidable sys.hasMonosyndetic

Equations

• Syntax.Coordination.instDecidableHasMonosyndetic sys = id inferInstance

def Syntax.Coordination.ConjunctionSystem.hasBisyndetic (sys : ConjunctionSystem) : Prop

Does a language attest at least one bisyndetic pattern?

Equations

• sys.hasBisyndetic = ∃ (p : Syntax.Coordination.CoordPattern), p ∈ sys.patterns ∧ p.syndesis = Syntax.Coordination.Syndesis.bisyndetic

@[implicit_reducible]

instance Syntax.Coordination.instDecidableHasBisyndetic (sys : ConjunctionSystem) : Decidable sys.hasBisyndetic

Equations

• Syntax.Coordination.instDecidableHasBisyndetic sys = id inferInstance

def Syntax.Coordination.ConjunctionSystem.muBoundness (sys : ConjunctionSystem) : Option Boundness

The boundness of a language's MU particle, if it has one.

Equations

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

Coordinate-structure symmetry

inductive Syntax.Coordination.CoordSymmetry : Type

Structural symmetry of a coordinate phrase (&P): whether one conjunct is structurally more prominent (c-commands the other) or the structure is flat / multidominant. The three groups of analyses for selection-violating coordination ([Sch26]) disagree on this parameter:

• Bottom-up accounts assume asymmetric: the first conjunct c-commands the second, so only it must satisfy the selector's c-selectional requirements.
• Linear/temporal-closeness accounts are compatible with either; their predictions derive from linear/temporal order, not structure.
• Symmetric accounts ([NPTvdK22], [Prz24]) posit flat or multidominance structures with no structural prominence.

• symmetric : CoordSymmetry

  Flat or multidominance: no conjunct is structurally more prominent.

• asymmetric : CoordSymmetry

  Binary &P: the first conjunct c-commands the second.

@[implicit_reducible]

instance Syntax.Coordination.instDecidableEqCoordSymmetry : DecidableEq CoordSymmetry

Equations

• Syntax.Coordination.instDecidableEqCoordSymmetry x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Syntax.Coordination.instReprCoordSymmetry.repr : CoordSymmetry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Coordination.instReprCoordSymmetry : Repr CoordSymmetry

Equations

• Syntax.Coordination.instReprCoordSymmetry = { reprPrec := Syntax.Coordination.instReprCoordSymmetry.repr }

@[implicit_reducible]

instance Syntax.Coordination.instBEqCoordSymmetry : BEq CoordSymmetry

Equations

• Syntax.Coordination.instBEqCoordSymmetry = { beq := Syntax.Coordination.instBEqCoordSymmetry.beq }

def Syntax.Coordination.instBEqCoordSymmetry.beq : CoordSymmetry → CoordSymmetry → Bool

Equations

• Syntax.Coordination.instBEqCoordSymmetry.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)