Classification Value

SE.Persistence.Domain.ClassificationValue

The values a persistence classification takes at an applicable transformation.

Inapplicability is not a value. It is the absence of a classification, and is represented by none in SE.Persistence.Classification.pattern.

inductive SE.Persistence.ClassificationValue : Type

Identity-persistence classification of an applicable transformation relative to one criterion of identity.

• ign: applicable and identity-ignoring (written IGN in the papers, and NEU in SE-200).
• prs: applicable and identity-preserving.
• brk: applicable and identity-breaking.

Inapplicable (N/A) is deliberately not a constructor; see SE.Persistence.Classification.

• ign : ClassificationValue
• prs : ClassificationValue
• brk : ClassificationValue

@[implicit_reducible]

instance SE.Persistence.instDecidableEqClassificationValue : DecidableEq ClassificationValue

Equations

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

@[implicit_reducible]

instance SE.Persistence.instReprClassificationValue : Repr ClassificationValue

Equations

• SE.Persistence.instReprClassificationValue = { reprPrec := SE.Persistence.instReprClassificationValue.repr }

def SE.Persistence.instReprClassificationValue.repr : ClassificationValue → Nat → Std.Format

Equations

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