eval_context.rs:184–212 mir_assign_valid_types. Equal canonical types short-circuit the relation; other pairs require exact rustc Covariant evidence. Successful relation checks retain the source layout-equality assertion.

def Miri.Input.CompilerCovariance.relationWithIndex {raw : Lean.Json} (index : CompilerQueryIndices.Covariance raw) (source target : MIR.TyId) : Except String Bool

Equations

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

def Miri.Input.CompilerCovariance.relation (p : CompilerProviders.Prepared) (source target : MIR.TyId) : Except String Bool

Equations

• Miri.Input.CompilerCovariance.relation p source target = Miri.Input.CompilerCovariance.relationWithIndex p.covarianceIndex source target

def Miri.Input.CompilerCovariance.compatible (p : CompilerProviders.Prepared) (debugAssertions : Bool) (source target : Interpreter.LocalLayout) : Except Interpreter.StepError Bool

Equations

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

def Miri.Input.CompilerCovariance.hook {S : Type} (p : CompilerProviders.Prepared) (debugAssertions : Bool) (source target : Interpreter.LocalLayout) : EStateM Interpreter.StepError S Bool

Equations

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