Structural operand coordinates within one source MIR instruction envelope. These identify source positions, never operand values, source spans, or an execution counter. The body and location are read from the current frame at actual constant evaluation.

inductive Miri.Interpreter.OperandPathElement : Type

• field (name : String) : OperandPathElement
• index (value : Nat) : OperandPathElement

def Miri.Interpreter.instReprOperandPathElement.repr : OperandPathElement → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprOperandPathElement : Repr OperandPathElement

Equations

• Miri.Interpreter.instReprOperandPathElement = { reprPrec := Miri.Interpreter.instReprOperandPathElement.repr }

def Miri.Interpreter.instDecidableEqOperandPathElement.decEq (x✝ x✝¹ : OperandPathElement) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.instDecidableEqOperandPathElement.decEq (Miri.Interpreter.OperandPathElement.field name) (Miri.Interpreter.OperandPathElement.index value) = isFalse ⋯
• Miri.Interpreter.instDecidableEqOperandPathElement.decEq (Miri.Interpreter.OperandPathElement.index value) (Miri.Interpreter.OperandPathElement.field name) = isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqOperandPathElement : DecidableEq OperandPathElement

Equations

• Miri.Interpreter.instDecidableEqOperandPathElement = Miri.Interpreter.instDecidableEqOperandPathElement.decEq

@[reducible, inline]

abbrev Miri.Interpreter.OperandPath : Type

Equations

• Miri.Interpreter.OperandPath = Array Miri.Interpreter.OperandPathElement

def Miri.Interpreter.OperandPath.instruction (field : String) : OperandPath

Equations

• Miri.Interpreter.OperandPath.instruction field = #[Miri.Interpreter.OperandPathElement.field "kind", Miri.Interpreter.OperandPathElement.field field]

def Miri.Interpreter.OperandPath.rvalue (field : String) : OperandPath

Equations

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

def Miri.Interpreter.OperandPath.aggregate (index : Nat) : OperandPath

Equations

• Miri.Interpreter.OperandPath.aggregate index = Array.push (Miri.Interpreter.OperandPath.rvalue "operands") (Miri.Interpreter.OperandPathElement.index index)

def Miri.Interpreter.OperandPath.argument (index : Nat) : OperandPath

Equations

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

def Miri.Interpreter.OperandPath.assertion (field : String) : OperandPath

Equations

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