Composition

SE.Transformation.Relation.Composition

Vocabulary for sequencing relationships among transformation operators.

This module defines the possible relation values only. The canonical known pairs are supplied by the explicitly partial lookup in SE.Transformation.Reference.Composition.

Composition describes sequencing.

inductive SE.Transformation.CompositionRelation : Type

Relationship describing whether one transformation operator may meaningfully follow another.

Absence of a canonical rule is represented by none in the lookup, not by a relation constructor.

• absorbing : CompositionRelation

  The second operator dominates, erases, or absorbs the first.

• composable : CompositionRelation

  The operator sequence is generally meaningful.

• conditionallyComposable : CompositionRelation

  The operator sequence is meaningful only under additional constraints.

• inverseLike : CompositionRelation

  The operators move in opposing directions but may not fully reverse.

• nonComposable : CompositionRelation

  The operator sequence is structurally invalid or incoherent.

• redundant : CompositionRelation

  The second operator adds no relevant structural change.

@[instance_reducible]

instance SE.Transformation.instDecidableEqCompositionRelation : DecidableEq CompositionRelation

Equations

• SE.Transformation.instDecidableEqCompositionRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def SE.Transformation.instReprCompositionRelation.repr : CompositionRelation → Nat → Std.Format

Equations

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

@[instance_reducible]

instance SE.Transformation.instReprCompositionRelation : Repr CompositionRelation

Equations

• SE.Transformation.instReprCompositionRelation = { reprPrec := SE.Transformation.instReprCompositionRelation.repr }