structure Strata.Python.Specs.WarningKind : Type

A warning category for PySpec translation. Uses an open vocabulary (string fields) so new categories can be added without modifying an inductive type.

• phase : String
• category : String

@[implicit_reducible]

instance Strata.Python.Specs.instBEqWarningKind : BEq WarningKind

Equations

• Strata.Python.Specs.instBEqWarningKind = { beq := Strata.Python.Specs.instBEqWarningKind.beq }

def Strata.Python.Specs.instBEqWarningKind.beq : WarningKind → WarningKind → Bool

Equations

• Strata.Python.Specs.instBEqWarningKind.beq { phase := a, category := a_1 } { phase := b, category := b_1 } = (a == b && a_1 == b_1)
• Strata.Python.Specs.instBEqWarningKind.beq x✝¹ x✝ = false

def Strata.Python.Specs.instDecidableEqWarningKind.decEq (x✝ x✝¹ : WarningKind) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Strata.Python.Specs.instDecidableEqWarningKind : DecidableEq WarningKind

Equations

• Strata.Python.Specs.instDecidableEqWarningKind = Strata.Python.Specs.instDecidableEqWarningKind.decEq

@[implicit_reducible]

instance Strata.Python.Specs.instHashableWarningKind : Hashable WarningKind

Equations

• Strata.Python.Specs.instHashableWarningKind = { hash := Strata.Python.Specs.instHashableWarningKind.hash }

def Strata.Python.Specs.instHashableWarningKind.hash : WarningKind → UInt64

Equations

• Strata.Python.Specs.instHashableWarningKind.hash { phase := a, category := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[implicit_reducible]

instance Strata.Python.Specs.instOrdWarningKind : Ord WarningKind

Equations

• Strata.Python.Specs.instOrdWarningKind = { compare := Strata.Python.Specs.instOrdWarningKind.ord }

def Strata.Python.Specs.instOrdWarningKind.ord : WarningKind → WarningKind → Ordering

Equations

• Strata.Python.Specs.instOrdWarningKind.ord { phase := a, category := a_1 } { phase := b, category := b_1 } = (compare a b).then ((compare a_1 b_1).then Ordering.eq)

@[implicit_reducible]

instance Strata.Python.Specs.instReprWarningKind : Repr WarningKind

Equations

• Strata.Python.Specs.instReprWarningKind = { reprPrec := Strata.Python.Specs.instReprWarningKind.repr }

def Strata.Python.Specs.instReprWarningKind.repr : WarningKind → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Strata.Python.Specs.instLTWarningKind : LT WarningKind

Equations

• Strata.Python.Specs.instLTWarningKind = { lt := fun (a b : Strata.Python.Specs.WarningKind) => a.phase < b.phase ∨ (a.phase == b.phase) = true ∧ a.category < b.category }

@[implicit_reducible]

instance Strata.Python.Specs.instDecidableLtWarningKind (a b : WarningKind) : Decidable (a < b)

Equations

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

def Strata.Python.Specs.WarningKind.unsupportedUnion : WarningKind

Equations

• Strata.Python.Specs.WarningKind.unsupportedUnion = { phase := "pySpecToLaurel", category := "unsupportedUnion" }

def Strata.Python.Specs.WarningKind.unsupportedOptionalFloat : WarningKind

Equations

• Strata.Python.Specs.WarningKind.unsupportedOptionalFloat = { phase := "pySpecToLaurel", category := "unsupportedOptionalFloat" }

def Strata.Python.Specs.WarningKind.unsupportedOptionalList : WarningKind

Equations

• Strata.Python.Specs.WarningKind.unsupportedOptionalList = { phase := "pySpecToLaurel", category := "unsupportedOptionalList" }

def Strata.Python.Specs.WarningKind.unsupportedOptionalDict : WarningKind

Equations

• Strata.Python.Specs.WarningKind.unsupportedOptionalDict = { phase := "pySpecToLaurel", category := "unsupportedOptionalDict" }

def Strata.Python.Specs.WarningKind.unsupportedOptionalAny : WarningKind

Equations

• Strata.Python.Specs.WarningKind.unsupportedOptionalAny = { phase := "pySpecToLaurel", category := "unsupportedOptionalAny" }

def Strata.Python.Specs.WarningKind.unsupportedOptionalBytes : WarningKind

Equations

• Strata.Python.Specs.WarningKind.unsupportedOptionalBytes = { phase := "pySpecToLaurel", category := "unsupportedOptionalBytes" }

def Strata.Python.Specs.WarningKind.typeError : WarningKind

Equations

• Strata.Python.Specs.WarningKind.typeError = { phase := "pySpecToLaurel", category := "typeError" }

def Strata.Python.Specs.WarningKind.placeholderExpr : WarningKind

Equations

• Strata.Python.Specs.WarningKind.placeholderExpr = { phase := "pySpecToLaurel", category := "placeholderExpr" }

def Strata.Python.Specs.WarningKind.floatLiteral : WarningKind

Equations

• Strata.Python.Specs.WarningKind.floatLiteral = { phase := "pySpecToLaurel", category := "floatLiteral" }

def Strata.Python.Specs.WarningKind.isinstanceUnsupported : WarningKind

Equations

• Strata.Python.Specs.WarningKind.isinstanceUnsupported = { phase := "pySpecToLaurel", category := "isinstanceUnsupported" }

def Strata.Python.Specs.WarningKind.forallListUnsupported : WarningKind

Equations

• Strata.Python.Specs.WarningKind.forallListUnsupported = { phase := "pySpecToLaurel", category := "forallListUnsupported" }

def Strata.Python.Specs.WarningKind.forallDictUnsupported : WarningKind

Equations

• Strata.Python.Specs.WarningKind.forallDictUnsupported = { phase := "pySpecToLaurel", category := "forallDictUnsupported" }

def Strata.Python.Specs.WarningKind.missingMethodSelf : WarningKind

Equations

• Strata.Python.Specs.WarningKind.missingMethodSelf = { phase := "pySpecToLaurel", category := "missingMethodSelf" }

def Strata.Python.Specs.WarningKind.kwargsExpansionError : WarningKind

Equations

• Strata.Python.Specs.WarningKind.kwargsExpansionError = { phase := "pySpecToLaurel", category := "kwargsExpansionError" }

def Strata.Python.Specs.WarningKind.postconditionUnsupported : WarningKind

Equations

• Strata.Python.Specs.WarningKind.postconditionUnsupported = { phase := "pySpecToLaurel", category := "postconditionUnsupported" }

def Strata.Python.Specs.WarningKind.overloadNoArgs : WarningKind

Equations

• Strata.Python.Specs.WarningKind.overloadNoArgs = { phase := "pySpecToLaurel", category := "overloadNoArgs" }

def Strata.Python.Specs.WarningKind.overloadArgArity : WarningKind

Equations

• Strata.Python.Specs.WarningKind.overloadArgArity = { phase := "pySpecToLaurel", category := "overloadArgArity" }

def Strata.Python.Specs.WarningKind.overloadArgNotStringLiteral : WarningKind

Equations

• Strata.Python.Specs.WarningKind.overloadArgNotStringLiteral = { phase := "pySpecToLaurel", category := "overloadArgNotStringLiteral" }

def Strata.Python.Specs.WarningKind.overloadReturnArity : WarningKind

Equations

• Strata.Python.Specs.WarningKind.overloadReturnArity = { phase := "pySpecToLaurel", category := "overloadReturnArity" }

def Strata.Python.Specs.WarningKind.overloadReturnNotClass : WarningKind

Equations

• Strata.Python.Specs.WarningKind.overloadReturnNotClass = { phase := "pySpecToLaurel", category := "overloadReturnNotClass" }

def Strata.Python.Specs.WarningKind.pySpecParsingError : WarningKind

Equations

• Strata.Python.Specs.WarningKind.pySpecParsingError = { phase := "pySpecParsing", category := "error" }

def Strata.Python.Specs.WarningKind.pySpecParsingWarning : WarningKind

Equations

• Strata.Python.Specs.WarningKind.pySpecParsingWarning = { phase := "pySpecParsing", category := "warning" }

structure Strata.Python.Specs.SpecError : Type

An error encountered while processing a PySpec file.

• file : System.FilePath
• loc : SourceRange
• kind : WarningKind
• message : String