inductive SE.Transformation.TransformationKind : Type

Broad behavioral category of transformation. Each transformation family belongs to exactly one transformation kind.

• contextual : TransformationKind
• normative : TransformationKind
• observational : TransformationKind
• organizational : TransformationKind
• relational : TransformationKind
• structural : TransformationKind
• temporal : TransformationKind

@[implicit_reducible]

instance SE.Transformation.instDecidableEqTransformationKind : DecidableEq TransformationKind

Equations

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

def SE.Transformation.instReprTransformationKind.repr : TransformationKind → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance SE.Transformation.instReprTransformationKind : Repr TransformationKind

Equations

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