Identity of an actual compiler MIR body in the fixed program's body table. This is independent of structural body equality, diagnostic names or spans.

structure Miri.Interpreter.BodyIdentity : Type

• index : Nat

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqBodyIdentity : DecidableEq BodyIdentity

Equations

• Miri.Interpreter.instDecidableEqBodyIdentity = Miri.Interpreter.instDecidableEqBodyIdentity.decEq

def Miri.Interpreter.instDecidableEqBodyIdentity.decEq (x✝ x✝¹ : BodyIdentity) : Decidable (x✝ = x✝¹)

Equations

• Miri.Interpreter.instDecidableEqBodyIdentity.decEq { index := a } { index := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.instReprBodyIdentity.repr : BodyIdentity → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instReprBodyIdentity : Repr BodyIdentity

Equations

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

def Miri.Interpreter.BodyIdentity.ofCanonicalIndex (index : Nat) : BodyIdentity

Called by the program loader with its exact compilation-local body key.

Equations

• Miri.Interpreter.BodyIdentity.ofCanonicalIndex index = { index := index }

structure Miri.Interpreter.LoadedBody : Type

• identity : BodyIdentity
• body : MIR.Body

def Miri.Interpreter.instDecidableEqLoadedBody.decEq (x✝ x✝¹ : LoadedBody) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqLoadedBody : DecidableEq LoadedBody

Equations

• Miri.Interpreter.instDecidableEqLoadedBody = Miri.Interpreter.instDecidableEqLoadedBody.decEq

@[instance_reducible]

instance Miri.Interpreter.instReprLoadedBody : Repr LoadedBody

Equations

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

def Miri.Interpreter.instReprLoadedBody.repr : LoadedBody → Nat → Std.Format

Equations

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