Operator Codes

ASCII-safe operator codes for Transformation theory.

These codes name kinds of change. They do not determine persistence.

inductive SE.Transformation.OperatorCode : Type

Canonical two-letter code identifying a transformation operator.

• AT : OperatorCode
• AZ : OperatorCode
• BD : OperatorCode
• BR : OperatorCode
• CL : OperatorCode
• CP : OperatorCode
• EM : OperatorCode
• EX : OperatorCode
• LK : OperatorCode
• MG : OperatorCode
• PR : OperatorCode
• RO : OperatorCode
• RV : OperatorCode
• SH : OperatorCode
• SP : OperatorCode
• UB : OperatorCode
• VS : OperatorCode

@[implicit_reducible]

instance SE.Transformation.instDecidableEqOperatorCode : DecidableEq OperatorCode

Equations

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

def SE.Transformation.instReprOperatorCode.repr : OperatorCode → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance SE.Transformation.instReprOperatorCode : Repr OperatorCode

Equations

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