Clause embedding contexts

This file defines Clause.Embedding, the [BD20] / [Day25] question-embedding contexts. Features.QParticleLayer is defined over these cells, so a particle's layer is derivable from its embedding distribution (Studies/BhattDayal2020).

inductive Clause.Embedding : Type

A [BD20] interrogative-embedding context.

• matrix : Embedding
• subordinated : Embedding
• quasiSubordinated : Embedding

  Embedded root-like interrogatives (Hindi-Urdu kya:).

• quotation : Embedding

@[implicit_reducible]

instance Clause.instDecidableEqEmbedding : DecidableEq Embedding

Equations

• Clause.instDecidableEqEmbedding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Clause.instReprEmbedding : Repr Embedding

Equations

• Clause.instReprEmbedding = { reprPrec := Clause.instReprEmbedding.repr }

def Clause.instReprEmbedding.repr : Embedding → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Clause.instReprEmbedding.repr Clause.Embedding.matrix prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Clause.Embedding.matrix")).group prec✝
• Clause.instReprEmbedding.repr Clause.Embedding.quotation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Clause.Embedding.quotation")).group prec✝