Cross-linguistic conditional markers

@cite{cao-white-lassiter-2025} @cite{mizuno-2024}

Typological vocabulary for conditional markers across languages. Some languages have distinct lexical items for hypothetical (HC) vs premise (PC) conditionals; others use a single marker for both. This file provides the marker-type inductive and the per-marker structure; per-language marker entries live in Fragments/{Language}/Conditionals.lean.

Extracted from Conditionals/ConditionalType.lean (was lines 372–396).

inductive Semantics.Conditionals.ConditionalMarkerType : Type

Cross-linguistic conditional markers and their type restrictions.

Some languages have distinct lexical items for HC vs PC conditionals. This captures the typological pattern.

Note: pcOnly is currently uninstantiated across known languages; included for typological completeness.

• hcOnly : ConditionalMarkerType

  Only marks HCs (e.g., Japanese -ra, German falls).

• pcOnly : ConditionalMarkerType

  Only marks PCs (currently uninstantiated).

• both : ConditionalMarkerType

  Can mark either (e.g., English "if", German wenn).

@[implicit_reducible]

instance Semantics.Conditionals.instDecidableEqConditionalMarkerType : DecidableEq ConditionalMarkerType

Equations

• Semantics.Conditionals.instDecidableEqConditionalMarkerType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Conditionals.instReprConditionalMarkerType : Repr ConditionalMarkerType

Equations

• Semantics.Conditionals.instReprConditionalMarkerType = { reprPrec := Semantics.Conditionals.instReprConditionalMarkerType.repr }

def Semantics.Conditionals.instReprConditionalMarkerType.repr : ConditionalMarkerType → Nat → Std.Format

Equations

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

structure Semantics.Conditionals.ConditionalMarker : Type

Cross-linguistic conditional marker datum.

Per-language marker entries live in Fragments/{Language}/Conditionals.lean.

• language : String
• marker : String
• gloss : String
• markerType : ConditionalMarkerType
• notes : String

def Semantics.Conditionals.instReprConditionalMarker.repr : ConditionalMarker → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Conditionals.instReprConditionalMarker : Repr ConditionalMarker

Equations

• Semantics.Conditionals.instReprConditionalMarker = { reprPrec := Semantics.Conditionals.instReprConditionalMarker.repr }