Elaboration-time input reflection. Generated declarations contain typed constructor values, not an opaque call to the IO decoder. This front end is part of the input trust boundary; importing data does not establish safety.

@[noinline]

def Miri.Frontend.checkedSome {α : Type} (value : Option α) (success : value.isSome = true) : α

Extract only with a kernel-checked witness of success. No default value.

Equations

• Miri.Frontend.checkedSome value success = value.get success

@[noinline]

def Miri.Frontend.checkedAllocId (value : UInt64) (success : (Memory.AllocId.ofUInt64 value).isSome = true) : Memory.AllocId

Equations

• Miri.Frontend.checkedAllocId value success = Miri.Frontend.checkedSome (Miri.Memory.AllocId.ofUInt64 value) success

@[noinline]

def Miri.Frontend.checkedCtfe (id : Memory.AllocId) (immutable sharedRef : Bool) (success : (Memory.CtfeProvenance.fromParts (id, immutable, sharedRef)).toOption.isSome = true) : Memory.CtfeProvenance

Equations

• Miri.Frontend.checkedCtfe id immutable sharedRef success = Miri.Frontend.checkedSome (Miri.Memory.CtfeProvenance.fromParts (id, immutable, sharedRef)).toOption success

@[instance_reducible]

instance Miri.Frontend.instToExprAllocId : Lean.ToExpr Memory.AllocId

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprCtfeProvenance : Lean.ToExpr Memory.CtfeProvenance

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprJsonNumber_miri : Lean.ToExpr Lean.JsonNumber

Equations

• Miri.Frontend.instToExprJsonNumber_miri = { toExpr := Miri.Frontend.instToExprJsonNumber_miri.toExpr, toTypeExpr := Lean.Expr.const `Lean.JsonNumber [] }

def Miri.Frontend.instToExprJsonNumber_miri.toExpr : Lean.JsonNumber → Lean.Expr

Equations

• Miri.Frontend.instToExprJsonNumber_miri.toExpr { mantissa := a, exponent := a_1 } = ((Lean.Expr.const `Lean.JsonNumber.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

@[instance_reducible]

instance Miri.Frontend.instToExprJson_miri : Lean.ToExpr Lean.Json

Equations

• Miri.Frontend.instToExprJson_miri = { toExpr := Miri.Frontend.jsonExpr✝ ∅, toTypeExpr := Lean.mkConst `Lean.Json }

@[instance_reducible]

instance Miri.Frontend.instToExprIntegerKind : Lean.ToExpr MIR.IntegerKind

Equations

• Miri.Frontend.instToExprIntegerKind = { toExpr := Miri.Frontend.instToExprIntegerKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.MIR.IntegerKind [] }

def Miri.Frontend.instToExprIntegerKind.toExpr : MIR.IntegerKind → Lean.Expr

Equations

• Miri.Frontend.instToExprIntegerKind.toExpr Miri.MIR.IntegerKind.i8 = Lean.Expr.const `Miri.MIR.IntegerKind.i8 []
• Miri.Frontend.instToExprIntegerKind.toExpr Miri.MIR.IntegerKind.i16 = Lean.Expr.const `Miri.MIR.IntegerKind.i16 []
• Miri.Frontend.instToExprIntegerKind.toExpr Miri.MIR.IntegerKind.i32 = Lean.Expr.const `Miri.MIR.IntegerKind.i32 []
• Miri.Frontend.instToExprIntegerKind.toExpr Miri.MIR.IntegerKind.i64 = Lean.Expr.const `Miri.MIR.IntegerKind.i64 []
• Miri.Frontend.instToExprIntegerKind.toExpr Miri.MIR.IntegerKind.i128 = Lean.Expr.const `Miri.MIR.IntegerKind.i128 []
• Miri.Frontend.instToExprIntegerKind.toExpr Miri.MIR.IntegerKind.isize = Lean.Expr.const `Miri.MIR.IntegerKind.isize []
• Miri.Frontend.instToExprIntegerKind.toExpr Miri.MIR.IntegerKind.u8 = Lean.Expr.const `Miri.MIR.IntegerKind.u8 []
• Miri.Frontend.instToExprIntegerKind.toExpr Miri.MIR.IntegerKind.u16 = Lean.Expr.const `Miri.MIR.IntegerKind.u16 []
• Miri.Frontend.instToExprIntegerKind.toExpr Miri.MIR.IntegerKind.u32 = Lean.Expr.const `Miri.MIR.IntegerKind.u32 []
• Miri.Frontend.instToExprIntegerKind.toExpr Miri.MIR.IntegerKind.u64 = Lean.Expr.const `Miri.MIR.IntegerKind.u64 []
• Miri.Frontend.instToExprIntegerKind.toExpr Miri.MIR.IntegerKind.u128 = Lean.Expr.const `Miri.MIR.IntegerKind.u128 []
• Miri.Frontend.instToExprIntegerKind.toExpr Miri.MIR.IntegerKind.usize = Lean.Expr.const `Miri.MIR.IntegerKind.usize []

@[instance_reducible]

instance Miri.Frontend.instToExprBinOp : Lean.ToExpr MIR.BinOp

Equations

• Miri.Frontend.instToExprBinOp = { toExpr := Miri.Frontend.instToExprBinOp.toExpr, toTypeExpr := Lean.Expr.const `Miri.MIR.BinOp [] }

def Miri.Frontend.instToExprBinOp.toExpr : MIR.BinOp → Lean.Expr

Equations

• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Add = Lean.Expr.const `Miri.MIR.BinOp.Add []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.AddUnchecked = Lean.Expr.const `Miri.MIR.BinOp.AddUnchecked []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.AddWithOverflow = Lean.Expr.const `Miri.MIR.BinOp.AddWithOverflow []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Sub = Lean.Expr.const `Miri.MIR.BinOp.Sub []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.SubUnchecked = Lean.Expr.const `Miri.MIR.BinOp.SubUnchecked []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.SubWithOverflow = Lean.Expr.const `Miri.MIR.BinOp.SubWithOverflow []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Mul = Lean.Expr.const `Miri.MIR.BinOp.Mul []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.MulUnchecked = Lean.Expr.const `Miri.MIR.BinOp.MulUnchecked []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.MulWithOverflow = Lean.Expr.const `Miri.MIR.BinOp.MulWithOverflow []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Div = Lean.Expr.const `Miri.MIR.BinOp.Div []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Rem = Lean.Expr.const `Miri.MIR.BinOp.Rem []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.BitXor = Lean.Expr.const `Miri.MIR.BinOp.BitXor []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.BitAnd = Lean.Expr.const `Miri.MIR.BinOp.BitAnd []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.BitOr = Lean.Expr.const `Miri.MIR.BinOp.BitOr []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Shl = Lean.Expr.const `Miri.MIR.BinOp.Shl []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.ShlUnchecked = Lean.Expr.const `Miri.MIR.BinOp.ShlUnchecked []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Shr = Lean.Expr.const `Miri.MIR.BinOp.Shr []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.ShrUnchecked = Lean.Expr.const `Miri.MIR.BinOp.ShrUnchecked []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Eq = Lean.Expr.const `Miri.MIR.BinOp.Eq []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Lt = Lean.Expr.const `Miri.MIR.BinOp.Lt []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Le = Lean.Expr.const `Miri.MIR.BinOp.Le []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Ne = Lean.Expr.const `Miri.MIR.BinOp.Ne []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Ge = Lean.Expr.const `Miri.MIR.BinOp.Ge []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Gt = Lean.Expr.const `Miri.MIR.BinOp.Gt []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Cmp = Lean.Expr.const `Miri.MIR.BinOp.Cmp []
• Miri.Frontend.instToExprBinOp.toExpr Miri.MIR.BinOp.Offset = Lean.Expr.const `Miri.MIR.BinOp.Offset []

@[instance_reducible]

instance Miri.Frontend.instToExprUnOp : Lean.ToExpr MIR.UnOp

Equations

• Miri.Frontend.instToExprUnOp = { toExpr := Miri.Frontend.instToExprUnOp.toExpr, toTypeExpr := Lean.Expr.const `Miri.MIR.UnOp [] }

def Miri.Frontend.instToExprUnOp.toExpr : MIR.UnOp → Lean.Expr

Equations

• Miri.Frontend.instToExprUnOp.toExpr Miri.MIR.UnOp.Not = Lean.Expr.const `Miri.MIR.UnOp.Not []
• Miri.Frontend.instToExprUnOp.toExpr Miri.MIR.UnOp.Neg = Lean.Expr.const `Miri.MIR.UnOp.Neg []
• Miri.Frontend.instToExprUnOp.toExpr Miri.MIR.UnOp.PtrMetadata = Lean.Expr.const `Miri.MIR.UnOp.PtrMetadata []

def Miri.Frontend.instToExprPayloadStatus.toExpr : Input.PayloadStatus → Lean.Expr

Equations

• Miri.Frontend.instToExprPayloadStatus.toExpr Miri.Input.PayloadStatus.supported = Lean.Expr.const `Miri.Input.PayloadStatus.supported []
• Miri.Frontend.instToExprPayloadStatus.toExpr Miri.Input.PayloadStatus.unsupported = Lean.Expr.const `Miri.Input.PayloadStatus.unsupported []
• Miri.Frontend.instToExprPayloadStatus.toExpr Miri.Input.PayloadStatus.unknown = Lean.Expr.const `Miri.Input.PayloadStatus.unknown []
• Miri.Frontend.instToExprPayloadStatus.toExpr Miri.Input.PayloadStatus.incomplete = Lean.Expr.const `Miri.Input.PayloadStatus.incomplete []
• Miri.Frontend.instToExprPayloadStatus.toExpr Miri.Input.PayloadStatus.debugPayload = Lean.Expr.const `Miri.Input.PayloadStatus.debugPayload []
• Miri.Frontend.instToExprPayloadStatus.toExpr (Miri.Input.PayloadStatus.unrecognized a) = (Lean.Expr.const `Miri.Input.PayloadStatus.unrecognized []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprPayloadStatus : Lean.ToExpr Input.PayloadStatus

Equations

• Miri.Frontend.instToExprPayloadStatus = { toExpr := Miri.Frontend.instToExprPayloadStatus.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.PayloadStatus [] }

def Miri.Frontend.instToExprTypeShapeKind.toExpr : Input.TypeShapeKind → Lean.Expr

Equations

• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.bool = Lean.Expr.const `Miri.Input.TypeShapeKind.bool []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.char = Lean.Expr.const `Miri.Input.TypeShapeKind.char []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.int = Lean.Expr.const `Miri.Input.TypeShapeKind.int []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.uint = Lean.Expr.const `Miri.Input.TypeShapeKind.uint []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.float = Lean.Expr.const `Miri.Input.TypeShapeKind.float []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.adt = Lean.Expr.const `Miri.Input.TypeShapeKind.adt []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.foreign = Lean.Expr.const `Miri.Input.TypeShapeKind.foreign []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.str = Lean.Expr.const `Miri.Input.TypeShapeKind.str []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.array = Lean.Expr.const `Miri.Input.TypeShapeKind.array []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.patternType = Lean.Expr.const `Miri.Input.TypeShapeKind.patternType []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.slice = Lean.Expr.const `Miri.Input.TypeShapeKind.slice []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.rawPointer = Lean.Expr.const `Miri.Input.TypeShapeKind.rawPointer []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.reference = Lean.Expr.const `Miri.Input.TypeShapeKind.reference []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.functionDefinition = Lean.Expr.const `Miri.Input.TypeShapeKind.functionDefinition []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.functionPointer = Lean.Expr.const `Miri.Input.TypeShapeKind.functionPointer []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.unsafeBinder = Lean.Expr.const `Miri.Input.TypeShapeKind.unsafeBinder []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.dynamicTraitObject = Lean.Expr.const `Miri.Input.TypeShapeKind.dynamicTraitObject []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.closure = Lean.Expr.const `Miri.Input.TypeShapeKind.closure []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.coroutineClosure = Lean.Expr.const `Miri.Input.TypeShapeKind.coroutineClosure []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.coroutine = Lean.Expr.const `Miri.Input.TypeShapeKind.coroutine []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.coroutineWitness = Lean.Expr.const `Miri.Input.TypeShapeKind.coroutineWitness []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.never = Lean.Expr.const `Miri.Input.TypeShapeKind.never []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.tuple = Lean.Expr.const `Miri.Input.TypeShapeKind.tuple []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.alias = Lean.Expr.const `Miri.Input.TypeShapeKind.alias []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.parameter = Lean.Expr.const `Miri.Input.TypeShapeKind.parameter []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.boundType = Lean.Expr.const `Miri.Input.TypeShapeKind.boundType []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.placeholderType = Lean.Expr.const `Miri.Input.TypeShapeKind.placeholderType []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.inferenceType = Lean.Expr.const `Miri.Input.TypeShapeKind.inferenceType []
• Miri.Frontend.instToExprTypeShapeKind.toExpr Miri.Input.TypeShapeKind.errorType = Lean.Expr.const `Miri.Input.TypeShapeKind.errorType []
• Miri.Frontend.instToExprTypeShapeKind.toExpr (Miri.Input.TypeShapeKind.unknown a) = (Lean.Expr.const `Miri.Input.TypeShapeKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprTypeShapeKind : Lean.ToExpr Input.TypeShapeKind

Equations

• Miri.Frontend.instToExprTypeShapeKind = { toExpr := Miri.Frontend.instToExprTypeShapeKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.TypeShapeKind [] }

def Miri.Frontend.instToExprStatementVariant.toExpr : Input.StatementVariant → Lean.Expr

Equations

• Miri.Frontend.instToExprStatementVariant.toExpr Miri.Input.StatementVariant.assign = Lean.Expr.const `Miri.Input.StatementVariant.assign []
• Miri.Frontend.instToExprStatementVariant.toExpr Miri.Input.StatementVariant.fakeRead = Lean.Expr.const `Miri.Input.StatementVariant.fakeRead []
• Miri.Frontend.instToExprStatementVariant.toExpr Miri.Input.StatementVariant.setDiscriminant = Lean.Expr.const `Miri.Input.StatementVariant.setDiscriminant []
• Miri.Frontend.instToExprStatementVariant.toExpr Miri.Input.StatementVariant.storageLive = Lean.Expr.const `Miri.Input.StatementVariant.storageLive []
• Miri.Frontend.instToExprStatementVariant.toExpr Miri.Input.StatementVariant.storageDead = Lean.Expr.const `Miri.Input.StatementVariant.storageDead []
• Miri.Frontend.instToExprStatementVariant.toExpr Miri.Input.StatementVariant.placeMention = Lean.Expr.const `Miri.Input.StatementVariant.placeMention []
• Miri.Frontend.instToExprStatementVariant.toExpr Miri.Input.StatementVariant.ascribeUserType = Lean.Expr.const `Miri.Input.StatementVariant.ascribeUserType []
• Miri.Frontend.instToExprStatementVariant.toExpr Miri.Input.StatementVariant.coverage = Lean.Expr.const `Miri.Input.StatementVariant.coverage []
• Miri.Frontend.instToExprStatementVariant.toExpr Miri.Input.StatementVariant.intrinsic = Lean.Expr.const `Miri.Input.StatementVariant.intrinsic []
• Miri.Frontend.instToExprStatementVariant.toExpr Miri.Input.StatementVariant.constEvalCounter = Lean.Expr.const `Miri.Input.StatementVariant.constEvalCounter []
• Miri.Frontend.instToExprStatementVariant.toExpr Miri.Input.StatementVariant.nop = Lean.Expr.const `Miri.Input.StatementVariant.nop []
• Miri.Frontend.instToExprStatementVariant.toExpr Miri.Input.StatementVariant.backwardIncompatibleDropHint = Lean.Expr.const `Miri.Input.StatementVariant.backwardIncompatibleDropHint []
• Miri.Frontend.instToExprStatementVariant.toExpr (Miri.Input.StatementVariant.unknown a) = (Lean.Expr.const `Miri.Input.StatementVariant.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprStatementVariant : Lean.ToExpr Input.StatementVariant

Equations

• Miri.Frontend.instToExprStatementVariant = { toExpr := Miri.Frontend.instToExprStatementVariant.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.StatementVariant [] }

def Miri.Frontend.instToExprTerminatorVariant.toExpr : Input.TerminatorVariant → Lean.Expr

Equations

• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.goto = Lean.Expr.const `Miri.Input.TerminatorVariant.goto []
• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.switchInt = Lean.Expr.const `Miri.Input.TerminatorVariant.switchInt []
• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.unwindResume = Lean.Expr.const `Miri.Input.TerminatorVariant.unwindResume []
• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.unwindTerminate = Lean.Expr.const `Miri.Input.TerminatorVariant.unwindTerminate []
• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.return = Lean.Expr.const `Miri.Input.TerminatorVariant.return []
• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.unreachable = Lean.Expr.const `Miri.Input.TerminatorVariant.unreachable []
• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.drop = Lean.Expr.const `Miri.Input.TerminatorVariant.drop []
• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.call = Lean.Expr.const `Miri.Input.TerminatorVariant.call []
• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.tailCall = Lean.Expr.const `Miri.Input.TerminatorVariant.tailCall []
• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.assert = Lean.Expr.const `Miri.Input.TerminatorVariant.assert []
• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.yield = Lean.Expr.const `Miri.Input.TerminatorVariant.yield []
• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.coroutineDrop = Lean.Expr.const `Miri.Input.TerminatorVariant.coroutineDrop []
• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.falseEdge = Lean.Expr.const `Miri.Input.TerminatorVariant.falseEdge []
• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.falseUnwind = Lean.Expr.const `Miri.Input.TerminatorVariant.falseUnwind []
• Miri.Frontend.instToExprTerminatorVariant.toExpr Miri.Input.TerminatorVariant.inlineAsm = Lean.Expr.const `Miri.Input.TerminatorVariant.inlineAsm []
• Miri.Frontend.instToExprTerminatorVariant.toExpr (Miri.Input.TerminatorVariant.unknown a) = (Lean.Expr.const `Miri.Input.TerminatorVariant.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprTerminatorVariant : Lean.ToExpr Input.TerminatorVariant

Equations

• Miri.Frontend.instToExprTerminatorVariant = { toExpr := Miri.Frontend.instToExprTerminatorVariant.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.TerminatorVariant [] }

@[instance_reducible]

instance Miri.Frontend.instToExprRvalueVariant : Lean.ToExpr Input.RvalueVariant

Equations

• Miri.Frontend.instToExprRvalueVariant = { toExpr := Miri.Frontend.instToExprRvalueVariant.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.RvalueVariant [] }

def Miri.Frontend.instToExprRvalueVariant.toExpr : Input.RvalueVariant → Lean.Expr

Equations

• Miri.Frontend.instToExprRvalueVariant.toExpr Miri.Input.RvalueVariant.use = Lean.Expr.const `Miri.Input.RvalueVariant.use []
• Miri.Frontend.instToExprRvalueVariant.toExpr Miri.Input.RvalueVariant.repeat = Lean.Expr.const `Miri.Input.RvalueVariant.repeat []
• Miri.Frontend.instToExprRvalueVariant.toExpr Miri.Input.RvalueVariant.ref = Lean.Expr.const `Miri.Input.RvalueVariant.ref []
• Miri.Frontend.instToExprRvalueVariant.toExpr Miri.Input.RvalueVariant.threadLocalRef = Lean.Expr.const `Miri.Input.RvalueVariant.threadLocalRef []
• Miri.Frontend.instToExprRvalueVariant.toExpr Miri.Input.RvalueVariant.rawPtr = Lean.Expr.const `Miri.Input.RvalueVariant.rawPtr []
• Miri.Frontend.instToExprRvalueVariant.toExpr Miri.Input.RvalueVariant.cast = Lean.Expr.const `Miri.Input.RvalueVariant.cast []
• Miri.Frontend.instToExprRvalueVariant.toExpr Miri.Input.RvalueVariant.binaryOp = Lean.Expr.const `Miri.Input.RvalueVariant.binaryOp []
• Miri.Frontend.instToExprRvalueVariant.toExpr Miri.Input.RvalueVariant.unaryOp = Lean.Expr.const `Miri.Input.RvalueVariant.unaryOp []
• Miri.Frontend.instToExprRvalueVariant.toExpr Miri.Input.RvalueVariant.discriminant = Lean.Expr.const `Miri.Input.RvalueVariant.discriminant []
• Miri.Frontend.instToExprRvalueVariant.toExpr Miri.Input.RvalueVariant.aggregate = Lean.Expr.const `Miri.Input.RvalueVariant.aggregate []
• Miri.Frontend.instToExprRvalueVariant.toExpr Miri.Input.RvalueVariant.copyForDeref = Lean.Expr.const `Miri.Input.RvalueVariant.copyForDeref []
• Miri.Frontend.instToExprRvalueVariant.toExpr Miri.Input.RvalueVariant.wrapUnsafeBinder = Lean.Expr.const `Miri.Input.RvalueVariant.wrapUnsafeBinder []
• Miri.Frontend.instToExprRvalueVariant.toExpr Miri.Input.RvalueVariant.reborrow = Lean.Expr.const `Miri.Input.RvalueVariant.reborrow []
• Miri.Frontend.instToExprRvalueVariant.toExpr (Miri.Input.RvalueVariant.unknown a) = (Lean.Expr.const `Miri.Input.RvalueVariant.unknown []).app (Lean.toExpr a)

def Miri.Frontend.instToExprOperandVariant.toExpr : Input.OperandVariant → Lean.Expr

Equations

• Miri.Frontend.instToExprOperandVariant.toExpr Miri.Input.OperandVariant.copy = Lean.Expr.const `Miri.Input.OperandVariant.copy []
• Miri.Frontend.instToExprOperandVariant.toExpr Miri.Input.OperandVariant.move = Lean.Expr.const `Miri.Input.OperandVariant.move []
• Miri.Frontend.instToExprOperandVariant.toExpr Miri.Input.OperandVariant.constant = Lean.Expr.const `Miri.Input.OperandVariant.constant []
• Miri.Frontend.instToExprOperandVariant.toExpr Miri.Input.OperandVariant.runtimeChecks = Lean.Expr.const `Miri.Input.OperandVariant.runtimeChecks []
• Miri.Frontend.instToExprOperandVariant.toExpr (Miri.Input.OperandVariant.unknown a) = (Lean.Expr.const `Miri.Input.OperandVariant.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprOperandVariant : Lean.ToExpr Input.OperandVariant

Equations

• Miri.Frontend.instToExprOperandVariant = { toExpr := Miri.Frontend.instToExprOperandVariant.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.OperandVariant [] }

@[instance_reducible]

instance Miri.Frontend.instToExprProjectionVariant : Lean.ToExpr Input.ProjectionVariant

Equations

• Miri.Frontend.instToExprProjectionVariant = { toExpr := Miri.Frontend.instToExprProjectionVariant.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.ProjectionVariant [] }

def Miri.Frontend.instToExprProjectionVariant.toExpr : Input.ProjectionVariant → Lean.Expr

Equations

• Miri.Frontend.instToExprProjectionVariant.toExpr Miri.Input.ProjectionVariant.deref = Lean.Expr.const `Miri.Input.ProjectionVariant.deref []
• Miri.Frontend.instToExprProjectionVariant.toExpr Miri.Input.ProjectionVariant.field = Lean.Expr.const `Miri.Input.ProjectionVariant.field []
• Miri.Frontend.instToExprProjectionVariant.toExpr Miri.Input.ProjectionVariant.index = Lean.Expr.const `Miri.Input.ProjectionVariant.index []
• Miri.Frontend.instToExprProjectionVariant.toExpr Miri.Input.ProjectionVariant.constantIndex = Lean.Expr.const `Miri.Input.ProjectionVariant.constantIndex []
• Miri.Frontend.instToExprProjectionVariant.toExpr Miri.Input.ProjectionVariant.subslice = Lean.Expr.const `Miri.Input.ProjectionVariant.subslice []
• Miri.Frontend.instToExprProjectionVariant.toExpr Miri.Input.ProjectionVariant.downcast = Lean.Expr.const `Miri.Input.ProjectionVariant.downcast []
• Miri.Frontend.instToExprProjectionVariant.toExpr Miri.Input.ProjectionVariant.opaqueCast = Lean.Expr.const `Miri.Input.ProjectionVariant.opaqueCast []
• Miri.Frontend.instToExprProjectionVariant.toExpr Miri.Input.ProjectionVariant.unwrapUnsafeBinder = Lean.Expr.const `Miri.Input.ProjectionVariant.unwrapUnsafeBinder []
• Miri.Frontend.instToExprProjectionVariant.toExpr Miri.Input.ProjectionVariant.phantomDeref = Lean.Expr.const `Miri.Input.ProjectionVariant.phantomDeref []
• Miri.Frontend.instToExprProjectionVariant.toExpr (Miri.Input.ProjectionVariant.unknown a) = (Lean.Expr.const `Miri.Input.ProjectionVariant.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprLayoutKind : Lean.ToExpr Input.LayoutKind

Equations

• Miri.Frontend.instToExprLayoutKind = { toExpr := Miri.Frontend.instToExprLayoutKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.LayoutKind [] }

def Miri.Frontend.instToExprLayoutKind.toExpr : Input.LayoutKind → Lean.Expr

Equations

• Miri.Frontend.instToExprLayoutKind.toExpr Miri.Input.LayoutKind.layout = Lean.Expr.const `Miri.Input.LayoutKind.layout []
• Miri.Frontend.instToExprLayoutKind.toExpr Miri.Input.LayoutKind.layoutQueryError = Lean.Expr.const `Miri.Input.LayoutKind.layoutQueryError []
• Miri.Frontend.instToExprLayoutKind.toExpr (Miri.Input.LayoutKind.unknown a) = (Lean.Expr.const `Miri.Input.LayoutKind.unknown []).app (Lean.toExpr a)

def Miri.Frontend.instToExprLayoutVariantsKind.toExpr : Input.LayoutVariantsKind → Lean.Expr

Equations

• Miri.Frontend.instToExprLayoutVariantsKind.toExpr Miri.Input.LayoutVariantsKind.single = Lean.Expr.const `Miri.Input.LayoutVariantsKind.single []
• Miri.Frontend.instToExprLayoutVariantsKind.toExpr Miri.Input.LayoutVariantsKind.multiple = Lean.Expr.const `Miri.Input.LayoutVariantsKind.multiple []
• Miri.Frontend.instToExprLayoutVariantsKind.toExpr Miri.Input.LayoutVariantsKind.empty = Lean.Expr.const `Miri.Input.LayoutVariantsKind.empty []
• Miri.Frontend.instToExprLayoutVariantsKind.toExpr (Miri.Input.LayoutVariantsKind.unknown a) = (Lean.Expr.const `Miri.Input.LayoutVariantsKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprLayoutVariantsKind : Lean.ToExpr Input.LayoutVariantsKind

Equations

• Miri.Frontend.instToExprLayoutVariantsKind = { toExpr := Miri.Frontend.instToExprLayoutVariantsKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.LayoutVariantsKind [] }

def Miri.Frontend.instToExprBackendReprKind.toExpr : Input.BackendReprKind → Lean.Expr

Equations

• Miri.Frontend.instToExprBackendReprKind.toExpr Miri.Input.BackendReprKind.scalar = Lean.Expr.const `Miri.Input.BackendReprKind.scalar []
• Miri.Frontend.instToExprBackendReprKind.toExpr Miri.Input.BackendReprKind.scalarPair = Lean.Expr.const `Miri.Input.BackendReprKind.scalarPair []
• Miri.Frontend.instToExprBackendReprKind.toExpr Miri.Input.BackendReprKind.memory = Lean.Expr.const `Miri.Input.BackendReprKind.memory []
• Miri.Frontend.instToExprBackendReprKind.toExpr Miri.Input.BackendReprKind.simdVector = Lean.Expr.const `Miri.Input.BackendReprKind.simdVector []
• Miri.Frontend.instToExprBackendReprKind.toExpr Miri.Input.BackendReprKind.scalableSimdVector = Lean.Expr.const `Miri.Input.BackendReprKind.scalableSimdVector []
• Miri.Frontend.instToExprBackendReprKind.toExpr (Miri.Input.BackendReprKind.unknown a) = (Lean.Expr.const `Miri.Input.BackendReprKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprBackendReprKind : Lean.ToExpr Input.BackendReprKind

Equations

• Miri.Frontend.instToExprBackendReprKind = { toExpr := Miri.Frontend.instToExprBackendReprKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.BackendReprKind [] }

def Miri.Frontend.instToExprFieldShapeKind.toExpr : Input.FieldShapeKind → Lean.Expr

Equations

• Miri.Frontend.instToExprFieldShapeKind.toExpr Miri.Input.FieldShapeKind.primitive = Lean.Expr.const `Miri.Input.FieldShapeKind.primitive []
• Miri.Frontend.instToExprFieldShapeKind.toExpr Miri.Input.FieldShapeKind.union = Lean.Expr.const `Miri.Input.FieldShapeKind.union []
• Miri.Frontend.instToExprFieldShapeKind.toExpr Miri.Input.FieldShapeKind.array = Lean.Expr.const `Miri.Input.FieldShapeKind.array []
• Miri.Frontend.instToExprFieldShapeKind.toExpr Miri.Input.FieldShapeKind.arbitrary = Lean.Expr.const `Miri.Input.FieldShapeKind.arbitrary []
• Miri.Frontend.instToExprFieldShapeKind.toExpr (Miri.Input.FieldShapeKind.unknown a) = (Lean.Expr.const `Miri.Input.FieldShapeKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprFieldShapeKind : Lean.ToExpr Input.FieldShapeKind

Equations

• Miri.Frontend.instToExprFieldShapeKind = { toExpr := Miri.Frontend.instToExprFieldShapeKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.FieldShapeKind [] }

def Miri.Frontend.instToExprIntegerTypeTag.toExpr : Input.IntegerTypeTag → Lean.Expr

Equations

• Miri.Frontend.instToExprIntegerTypeTag.toExpr (Miri.Input.IntegerTypeTag.known a) = (Lean.Expr.const `Miri.Input.IntegerTypeTag.known []).app (Lean.toExpr a)
• Miri.Frontend.instToExprIntegerTypeTag.toExpr (Miri.Input.IntegerTypeTag.unknown a) = (Lean.Expr.const `Miri.Input.IntegerTypeTag.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprIntegerTypeTag : Lean.ToExpr Input.IntegerTypeTag

Equations

• Miri.Frontend.instToExprIntegerTypeTag = { toExpr := Miri.Frontend.instToExprIntegerTypeTag.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.IntegerTypeTag [] }

@[instance_reducible]

instance Miri.Frontend.instToExprFloatTypeTag : Lean.ToExpr Input.FloatTypeTag

Equations

• Miri.Frontend.instToExprFloatTypeTag = { toExpr := Miri.Frontend.instToExprFloatTypeTag.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.FloatTypeTag [] }

def Miri.Frontend.instToExprFloatTypeTag.toExpr : Input.FloatTypeTag → Lean.Expr

Equations

• Miri.Frontend.instToExprFloatTypeTag.toExpr Miri.Input.FloatTypeTag.f16 = Lean.Expr.const `Miri.Input.FloatTypeTag.f16 []
• Miri.Frontend.instToExprFloatTypeTag.toExpr Miri.Input.FloatTypeTag.f16b = Lean.Expr.const `Miri.Input.FloatTypeTag.f16b []
• Miri.Frontend.instToExprFloatTypeTag.toExpr Miri.Input.FloatTypeTag.f32 = Lean.Expr.const `Miri.Input.FloatTypeTag.f32 []
• Miri.Frontend.instToExprFloatTypeTag.toExpr Miri.Input.FloatTypeTag.f64 = Lean.Expr.const `Miri.Input.FloatTypeTag.f64 []
• Miri.Frontend.instToExprFloatTypeTag.toExpr Miri.Input.FloatTypeTag.f128 = Lean.Expr.const `Miri.Input.FloatTypeTag.f128 []
• Miri.Frontend.instToExprFloatTypeTag.toExpr Miri.Input.FloatTypeTag.ppcf128 = Lean.Expr.const `Miri.Input.FloatTypeTag.ppcf128 []
• Miri.Frontend.instToExprFloatTypeTag.toExpr (Miri.Input.FloatTypeTag.unknown a) = (Lean.Expr.const `Miri.Input.FloatTypeTag.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprAdtKind : Lean.ToExpr Input.AdtKind

Equations

• Miri.Frontend.instToExprAdtKind = { toExpr := Miri.Frontend.instToExprAdtKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.AdtKind [] }

def Miri.Frontend.instToExprAdtKind.toExpr : Input.AdtKind → Lean.Expr

Equations

• Miri.Frontend.instToExprAdtKind.toExpr Miri.Input.AdtKind.structKind = Lean.Expr.const `Miri.Input.AdtKind.structKind []
• Miri.Frontend.instToExprAdtKind.toExpr Miri.Input.AdtKind.unionKind = Lean.Expr.const `Miri.Input.AdtKind.unionKind []
• Miri.Frontend.instToExprAdtKind.toExpr Miri.Input.AdtKind.enumKind = Lean.Expr.const `Miri.Input.AdtKind.enumKind []
• Miri.Frontend.instToExprAdtKind.toExpr (Miri.Input.AdtKind.unknown a) = (Lean.Expr.const `Miri.Input.AdtKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprTypeShapeMetadata : Lean.ToExpr Input.TypeShapeMetadata

Equations

• Miri.Frontend.instToExprTypeShapeMetadata = { toExpr := Miri.Frontend.instToExprTypeShapeMetadata.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.TypeShapeMetadata [] }

def Miri.Frontend.instToExprTypeShapeMetadata.toExpr : Input.TypeShapeMetadata → Lean.Expr

Equations

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

def Miri.Frontend.instToExprPrimitiveKind.toExpr : Input.PrimitiveKind → Lean.Expr

Equations

• Miri.Frontend.instToExprPrimitiveKind.toExpr Miri.Input.PrimitiveKind.integer = Lean.Expr.const `Miri.Input.PrimitiveKind.integer []
• Miri.Frontend.instToExprPrimitiveKind.toExpr Miri.Input.PrimitiveKind.float = Lean.Expr.const `Miri.Input.PrimitiveKind.float []
• Miri.Frontend.instToExprPrimitiveKind.toExpr Miri.Input.PrimitiveKind.pointer = Lean.Expr.const `Miri.Input.PrimitiveKind.pointer []
• Miri.Frontend.instToExprPrimitiveKind.toExpr (Miri.Input.PrimitiveKind.unknown a) = (Lean.Expr.const `Miri.Input.PrimitiveKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprPrimitiveKind : Lean.ToExpr Input.PrimitiveKind

Equations

• Miri.Frontend.instToExprPrimitiveKind = { toExpr := Miri.Frontend.instToExprPrimitiveKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.PrimitiveKind [] }

def Miri.Frontend.instToExprScalarShapeKind.toExpr : Input.ScalarShapeKind → Lean.Expr

Equations

• Miri.Frontend.instToExprScalarShapeKind.toExpr Miri.Input.ScalarShapeKind.initialized = Lean.Expr.const `Miri.Input.ScalarShapeKind.initialized []
• Miri.Frontend.instToExprScalarShapeKind.toExpr Miri.Input.ScalarShapeKind.union = Lean.Expr.const `Miri.Input.ScalarShapeKind.union []
• Miri.Frontend.instToExprScalarShapeKind.toExpr (Miri.Input.ScalarShapeKind.unknown a) = (Lean.Expr.const `Miri.Input.ScalarShapeKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprScalarShapeKind : Lean.ToExpr Input.ScalarShapeKind

Equations

• Miri.Frontend.instToExprScalarShapeKind = { toExpr := Miri.Frontend.instToExprScalarShapeKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.ScalarShapeKind [] }

def Miri.Frontend.instToExprPassModeKind.toExpr : Input.PassModeKind → Lean.Expr

Equations

• Miri.Frontend.instToExprPassModeKind.toExpr Miri.Input.PassModeKind.ignore = Lean.Expr.const `Miri.Input.PassModeKind.ignore []
• Miri.Frontend.instToExprPassModeKind.toExpr Miri.Input.PassModeKind.direct = Lean.Expr.const `Miri.Input.PassModeKind.direct []
• Miri.Frontend.instToExprPassModeKind.toExpr Miri.Input.PassModeKind.pair = Lean.Expr.const `Miri.Input.PassModeKind.pair []
• Miri.Frontend.instToExprPassModeKind.toExpr Miri.Input.PassModeKind.cast = Lean.Expr.const `Miri.Input.PassModeKind.cast []
• Miri.Frontend.instToExprPassModeKind.toExpr Miri.Input.PassModeKind.indirect = Lean.Expr.const `Miri.Input.PassModeKind.indirect []
• Miri.Frontend.instToExprPassModeKind.toExpr Miri.Input.PassModeKind.indirectUnsized = Lean.Expr.const `Miri.Input.PassModeKind.indirectUnsized []
• Miri.Frontend.instToExprPassModeKind.toExpr (Miri.Input.PassModeKind.unknown a) = (Lean.Expr.const `Miri.Input.PassModeKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprPassModeKind : Lean.ToExpr Input.PassModeKind

Equations

• Miri.Frontend.instToExprPassModeKind = { toExpr := Miri.Frontend.instToExprPassModeKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.PassModeKind [] }

def Miri.Frontend.instToExprAllocationKind.toExpr : Input.AllocationKind → Lean.Expr

Equations

• Miri.Frontend.instToExprAllocationKind.toExpr Miri.Input.AllocationKind.memory = Lean.Expr.const `Miri.Input.AllocationKind.memory []
• Miri.Frontend.instToExprAllocationKind.toExpr Miri.Input.AllocationKind.function = Lean.Expr.const `Miri.Input.AllocationKind.function []
• Miri.Frontend.instToExprAllocationKind.toExpr Miri.Input.AllocationKind.static = Lean.Expr.const `Miri.Input.AllocationKind.static []
• Miri.Frontend.instToExprAllocationKind.toExpr Miri.Input.AllocationKind.vtable = Lean.Expr.const `Miri.Input.AllocationKind.vtable []
• Miri.Frontend.instToExprAllocationKind.toExpr Miri.Input.AllocationKind.typeId = Lean.Expr.const `Miri.Input.AllocationKind.typeId []
• Miri.Frontend.instToExprAllocationKind.toExpr (Miri.Input.AllocationKind.other a) = (Lean.Expr.const `Miri.Input.AllocationKind.other []).app (Lean.toExpr a)
• Miri.Frontend.instToExprAllocationKind.toExpr Miri.Input.AllocationKind.unknown = Lean.Expr.const `Miri.Input.AllocationKind.unknown []

@[instance_reducible]

instance Miri.Frontend.instToExprAllocationKind : Lean.ToExpr Input.AllocationKind

Equations

• Miri.Frontend.instToExprAllocationKind = { toExpr := Miri.Frontend.instToExprAllocationKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.AllocationKind [] }

def Miri.Frontend.instToExprInstanceKind.toExpr : Input.InstanceKind → Lean.Expr

Equations

• Miri.Frontend.instToExprInstanceKind.toExpr Miri.Input.InstanceKind.instanceMir = Lean.Expr.const `Miri.Input.InstanceKind.instanceMir []
• Miri.Frontend.instToExprInstanceKind.toExpr Miri.Input.InstanceKind.instanceMirTemplate = Lean.Expr.const `Miri.Input.InstanceKind.instanceMirTemplate []
• Miri.Frontend.instToExprInstanceKind.toExpr Miri.Input.InstanceKind.intrinsicWithoutMir = Lean.Expr.const `Miri.Input.InstanceKind.intrinsicWithoutMir []
• Miri.Frontend.instToExprInstanceKind.toExpr Miri.Input.InstanceKind.intrinsicDispatch = Lean.Expr.const `Miri.Input.InstanceKind.intrinsicDispatch []
• Miri.Frontend.instToExprInstanceKind.toExpr Miri.Input.InstanceKind.foreignItemNoMir = Lean.Expr.const `Miri.Input.InstanceKind.foreignItemNoMir []
• Miri.Frontend.instToExprInstanceKind.toExpr Miri.Input.InstanceKind.virtualDispatch = Lean.Expr.const `Miri.Input.InstanceKind.virtualDispatch []
• Miri.Frontend.instToExprInstanceKind.toExpr Miri.Input.InstanceKind.virtualDispatchTarget = Lean.Expr.const `Miri.Input.InstanceKind.virtualDispatchTarget []
• Miri.Frontend.instToExprInstanceKind.toExpr Miri.Input.InstanceKind.instanceMirUnavailable = Lean.Expr.const `Miri.Input.InstanceKind.instanceMirUnavailable []
• Miri.Frontend.instToExprInstanceKind.toExpr Miri.Input.InstanceKind.symbolIdentityOnly = Lean.Expr.const `Miri.Input.InstanceKind.symbolIdentityOnly []
• Miri.Frontend.instToExprInstanceKind.toExpr (Miri.Input.InstanceKind.other a) = (Lean.Expr.const `Miri.Input.InstanceKind.other []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprInstanceKind : Lean.ToExpr Input.InstanceKind

Equations

• Miri.Frontend.instToExprInstanceKind = { toExpr := Miri.Frontend.instToExprInstanceKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.InstanceKind [] }

@[instance_reducible]

instance Miri.Frontend.instToExprObligation : Lean.ToExpr Input.Obligation

Equations

• Miri.Frontend.instToExprObligation = { toExpr := Miri.Frontend.instToExprObligation.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.Obligation [] }

def Miri.Frontend.instToExprObligation.toExpr : Input.Obligation → Lean.Expr

Equations

• Miri.Frontend.instToExprObligation.toExpr { path := a, message := a_1 } = ((Lean.Expr.const `Miri.Input.Obligation.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

def Miri.Frontend.instToExprSourcePosition.toExpr : Input.SourcePosition → Lean.Expr

Equations

• Miri.Frontend.instToExprSourcePosition.toExpr { line := a, column := a_1 } = ((Lean.Expr.const `Miri.Input.SourcePosition.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

@[instance_reducible]

instance Miri.Frontend.instToExprSourcePosition : Lean.ToExpr Input.SourcePosition

Equations

• Miri.Frontend.instToExprSourcePosition = { toExpr := Miri.Frontend.instToExprSourcePosition.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.SourcePosition [] }

@[instance_reducible]

instance Miri.Frontend.instToExprSourceSpanData : Lean.ToExpr Input.SourceSpanData

Equations

• Miri.Frontend.instToExprSourceSpanData = { toExpr := Miri.Frontend.instToExprSourceSpanData.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.SourceSpanData [] }

def Miri.Frontend.instToExprSourceSpanData.toExpr : Input.SourceSpanData → Lean.Expr

Equations

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

def Miri.Frontend.instToExprSourceInfo.toExpr : Input.SourceInfo → Lean.Expr

Equations

• Miri.Frontend.instToExprSourceInfo.toExpr { span := a, scope := a_1 } = ((Lean.Expr.const `Miri.Input.SourceInfo.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

@[instance_reducible]

instance Miri.Frontend.instToExprSourceInfo : Lean.ToExpr Input.SourceInfo

Equations

• Miri.Frontend.instToExprSourceInfo = { toExpr := Miri.Frontend.instToExprSourceInfo.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.SourceInfo [] }

def Miri.Frontend.instToExprProducer.toExpr : Input.Producer → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprProducer : Lean.ToExpr Input.Producer

Equations

• Miri.Frontend.instToExprProducer = { toExpr := Miri.Frontend.instToExprProducer.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.Producer [] }

@[instance_reducible]

instance Miri.Frontend.instToExprTaggedNode [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.TaggedNode

Equations

• Miri.Frontend.instToExprTaggedNode = { toExpr := Miri.Frontend.instToExprTaggedNode.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.TaggedNode [] }

def Miri.Frontend.instToExprTaggedNode.toExpr [Lean.ToExpr Lean.Json] : Input.TaggedNode → Lean.Expr

Equations

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

def Miri.Frontend.instToExprFieldShape.toExpr [Lean.ToExpr Lean.Json] : Input.FieldShape → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprFieldShape [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.FieldShape

Equations

• Miri.Frontend.instToExprFieldShape = { toExpr := Miri.Frontend.instToExprFieldShape.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.FieldShape [] }

@[instance_reducible]

instance Miri.Frontend.instToExprPrimitiveLayout [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.PrimitiveLayout

Equations

• Miri.Frontend.instToExprPrimitiveLayout = { toExpr := Miri.Frontend.instToExprPrimitiveLayout.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.PrimitiveLayout [] }

def Miri.Frontend.instToExprPrimitiveLayout.toExpr [Lean.ToExpr Lean.Json] : Input.PrimitiveLayout → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprScalarLayout [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.ScalarLayout

Equations

• Miri.Frontend.instToExprScalarLayout = { toExpr := Miri.Frontend.instToExprScalarLayout.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.ScalarLayout [] }

def Miri.Frontend.instToExprScalarLayout.toExpr [Lean.ToExpr Lean.Json] : Input.ScalarLayout → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprBackendRepr [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.BackendRepr

Equations

• Miri.Frontend.instToExprBackendRepr = { toExpr := Miri.Frontend.instToExprBackendRepr.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.BackendRepr [] }

def Miri.Frontend.instToExprBackendRepr.toExpr [Lean.ToExpr Lean.Json] : Input.BackendRepr → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprLayoutVariant [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.LayoutVariant

Equations

• Miri.Frontend.instToExprLayoutVariant = { toExpr := Miri.Frontend.instToExprLayoutVariant.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.LayoutVariant [] }

def Miri.Frontend.instToExprLayoutVariant.toExpr [Lean.ToExpr Lean.Json] : Input.LayoutVariant → Lean.Expr

Equations

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

def Miri.Frontend.instToExprTagEncodingKind.toExpr : Input.TagEncodingKind → Lean.Expr

Equations

• Miri.Frontend.instToExprTagEncodingKind.toExpr Miri.Input.TagEncodingKind.direct = Lean.Expr.const `Miri.Input.TagEncodingKind.direct []
• Miri.Frontend.instToExprTagEncodingKind.toExpr Miri.Input.TagEncodingKind.niche = Lean.Expr.const `Miri.Input.TagEncodingKind.niche []
• Miri.Frontend.instToExprTagEncodingKind.toExpr (Miri.Input.TagEncodingKind.unknown a) = (Lean.Expr.const `Miri.Input.TagEncodingKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprTagEncodingKind : Lean.ToExpr Input.TagEncodingKind

Equations

• Miri.Frontend.instToExprTagEncodingKind = { toExpr := Miri.Frontend.instToExprTagEncodingKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.TagEncodingKind [] }

def Miri.Frontend.instToExprTagEncoding.toExpr [Lean.ToExpr Lean.Json] : Input.TagEncoding → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprTagEncoding [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.TagEncoding

Equations

• Miri.Frontend.instToExprTagEncoding = { toExpr := Miri.Frontend.instToExprTagEncoding.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.TagEncoding [] }

@[instance_reducible]

instance Miri.Frontend.instToExprVariantsLayout [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.VariantsLayout

Equations

• Miri.Frontend.instToExprVariantsLayout = { toExpr := Miri.Frontend.instToExprVariantsLayout.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.VariantsLayout [] }

def Miri.Frontend.instToExprVariantsLayout.toExpr [Lean.ToExpr Lean.Json] : Input.VariantsLayout → Lean.Expr

Equations

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

def Miri.Frontend.instToExprLayout.toExpr [Lean.ToExpr Lean.Json] : Input.Layout → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprLayout [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.Layout

Equations

• Miri.Frontend.instToExprLayout = { toExpr := Miri.Frontend.instToExprLayout.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.Layout [] }

@[instance_reducible]

instance Miri.Frontend.instToExprExternAbi [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.ExternAbi

Equations

• Miri.Frontend.instToExprExternAbi = { toExpr := Miri.Frontend.instToExprExternAbi.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.ExternAbi [] }

def Miri.Frontend.instToExprExternAbi.toExpr [Lean.ToExpr Lean.Json] : Input.ExternAbi → Lean.Expr

Equations

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

def Miri.Frontend.instToExprArmCallKind.toExpr : Input.ArmCallKind → Lean.Expr

Equations

• Miri.Frontend.instToExprArmCallKind.toExpr Miri.Input.ArmCallKind.aapcs = Lean.Expr.const `Miri.Input.ArmCallKind.aapcs []
• Miri.Frontend.instToExprArmCallKind.toExpr Miri.Input.ArmCallKind.cmseNonSecureCall = Lean.Expr.const `Miri.Input.ArmCallKind.cmseNonSecureCall []
• Miri.Frontend.instToExprArmCallKind.toExpr Miri.Input.ArmCallKind.cmseNonSecureEntry = Lean.Expr.const `Miri.Input.ArmCallKind.cmseNonSecureEntry []
• Miri.Frontend.instToExprArmCallKind.toExpr (Miri.Input.ArmCallKind.unknown a) = (Lean.Expr.const `Miri.Input.ArmCallKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprArmCallKind : Lean.ToExpr Input.ArmCallKind

Equations

• Miri.Frontend.instToExprArmCallKind = { toExpr := Miri.Frontend.instToExprArmCallKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.ArmCallKind [] }

def Miri.Frontend.instToExprInterruptCallKind.toExpr : Input.InterruptCallKind → Lean.Expr

Equations

• Miri.Frontend.instToExprInterruptCallKind.toExpr Miri.Input.InterruptCallKind.avr = Lean.Expr.const `Miri.Input.InterruptCallKind.avr []
• Miri.Frontend.instToExprInterruptCallKind.toExpr Miri.Input.InterruptCallKind.avrNonBlocking = Lean.Expr.const `Miri.Input.InterruptCallKind.avrNonBlocking []
• Miri.Frontend.instToExprInterruptCallKind.toExpr Miri.Input.InterruptCallKind.msp430 = Lean.Expr.const `Miri.Input.InterruptCallKind.msp430 []
• Miri.Frontend.instToExprInterruptCallKind.toExpr Miri.Input.InterruptCallKind.riscvMachine = Lean.Expr.const `Miri.Input.InterruptCallKind.riscvMachine []
• Miri.Frontend.instToExprInterruptCallKind.toExpr Miri.Input.InterruptCallKind.riscvSupervisor = Lean.Expr.const `Miri.Input.InterruptCallKind.riscvSupervisor []
• Miri.Frontend.instToExprInterruptCallKind.toExpr Miri.Input.InterruptCallKind.x86 = Lean.Expr.const `Miri.Input.InterruptCallKind.x86 []
• Miri.Frontend.instToExprInterruptCallKind.toExpr (Miri.Input.InterruptCallKind.unknown a) = (Lean.Expr.const `Miri.Input.InterruptCallKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprInterruptCallKind : Lean.ToExpr Input.InterruptCallKind

Equations

• Miri.Frontend.instToExprInterruptCallKind = { toExpr := Miri.Frontend.instToExprInterruptCallKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.InterruptCallKind [] }

def Miri.Frontend.instToExprX86CallKind.toExpr : Input.X86CallKind → Lean.Expr

Equations

• Miri.Frontend.instToExprX86CallKind.toExpr Miri.Input.X86CallKind.fastcall = Lean.Expr.const `Miri.Input.X86CallKind.fastcall []
• Miri.Frontend.instToExprX86CallKind.toExpr Miri.Input.X86CallKind.stdcall = Lean.Expr.const `Miri.Input.X86CallKind.stdcall []
• Miri.Frontend.instToExprX86CallKind.toExpr Miri.Input.X86CallKind.sysv64 = Lean.Expr.const `Miri.Input.X86CallKind.sysv64 []
• Miri.Frontend.instToExprX86CallKind.toExpr Miri.Input.X86CallKind.thiscall = Lean.Expr.const `Miri.Input.X86CallKind.thiscall []
• Miri.Frontend.instToExprX86CallKind.toExpr Miri.Input.X86CallKind.vectorcall = Lean.Expr.const `Miri.Input.X86CallKind.vectorcall []
• Miri.Frontend.instToExprX86CallKind.toExpr Miri.Input.X86CallKind.win64 = Lean.Expr.const `Miri.Input.X86CallKind.win64 []
• Miri.Frontend.instToExprX86CallKind.toExpr (Miri.Input.X86CallKind.unknown a) = (Lean.Expr.const `Miri.Input.X86CallKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprX86CallKind : Lean.ToExpr Input.X86CallKind

Equations

• Miri.Frontend.instToExprX86CallKind = { toExpr := Miri.Frontend.instToExprX86CallKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.X86CallKind [] }

@[instance_reducible]

instance Miri.Frontend.instToExprCanonicalAbiKind : Lean.ToExpr Input.CanonicalAbiKind

Equations

• Miri.Frontend.instToExprCanonicalAbiKind = { toExpr := Miri.Frontend.instToExprCanonicalAbiKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.CanonicalAbiKind [] }

def Miri.Frontend.instToExprCanonicalAbiKind.toExpr : Input.CanonicalAbiKind → Lean.Expr

Equations

• Miri.Frontend.instToExprCanonicalAbiKind.toExpr Miri.Input.CanonicalAbiKind.c = Lean.Expr.const `Miri.Input.CanonicalAbiKind.c []
• Miri.Frontend.instToExprCanonicalAbiKind.toExpr Miri.Input.CanonicalAbiKind.rust = Lean.Expr.const `Miri.Input.CanonicalAbiKind.rust []
• Miri.Frontend.instToExprCanonicalAbiKind.toExpr Miri.Input.CanonicalAbiKind.rustCold = Lean.Expr.const `Miri.Input.CanonicalAbiKind.rustCold []
• Miri.Frontend.instToExprCanonicalAbiKind.toExpr Miri.Input.CanonicalAbiKind.rustPreserveNone = Lean.Expr.const `Miri.Input.CanonicalAbiKind.rustPreserveNone []
• Miri.Frontend.instToExprCanonicalAbiKind.toExpr Miri.Input.CanonicalAbiKind.rustTail = Lean.Expr.const `Miri.Input.CanonicalAbiKind.rustTail []
• Miri.Frontend.instToExprCanonicalAbiKind.toExpr Miri.Input.CanonicalAbiKind.custom = Lean.Expr.const `Miri.Input.CanonicalAbiKind.custom []
• Miri.Frontend.instToExprCanonicalAbiKind.toExpr Miri.Input.CanonicalAbiKind.swift = Lean.Expr.const `Miri.Input.CanonicalAbiKind.swift []
• Miri.Frontend.instToExprCanonicalAbiKind.toExpr Miri.Input.CanonicalAbiKind.arm = Lean.Expr.const `Miri.Input.CanonicalAbiKind.arm []
• Miri.Frontend.instToExprCanonicalAbiKind.toExpr Miri.Input.CanonicalAbiKind.gpuKernel = Lean.Expr.const `Miri.Input.CanonicalAbiKind.gpuKernel []
• Miri.Frontend.instToExprCanonicalAbiKind.toExpr Miri.Input.CanonicalAbiKind.interrupt = Lean.Expr.const `Miri.Input.CanonicalAbiKind.interrupt []
• Miri.Frontend.instToExprCanonicalAbiKind.toExpr Miri.Input.CanonicalAbiKind.x86 = Lean.Expr.const `Miri.Input.CanonicalAbiKind.x86 []
• Miri.Frontend.instToExprCanonicalAbiKind.toExpr (Miri.Input.CanonicalAbiKind.unknown a) = (Lean.Expr.const `Miri.Input.CanonicalAbiKind.unknown []).app (Lean.toExpr a)

def Miri.Frontend.instToExprCanonicalAbi.toExpr [Lean.ToExpr Lean.Json] : Input.CanonicalAbi → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprCanonicalAbi [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.CanonicalAbi

Equations

• Miri.Frontend.instToExprCanonicalAbi = { toExpr := Miri.Frontend.instToExprCanonicalAbi.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.CanonicalAbi [] }

@[instance_reducible]

instance Miri.Frontend.instToExprTypedEnumTag : Lean.ToExpr Input.TypedEnumTag

Equations

• Miri.Frontend.instToExprTypedEnumTag = { toExpr := Miri.Frontend.instToExprTypedEnumTag.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.TypedEnumTag [] }

def Miri.Frontend.instToExprTypedEnumTag.toExpr : Input.TypedEnumTag → Lean.Expr

Equations

• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.safety = Lean.Expr.const `Miri.Input.TypedEnumTag.safety []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.borrowKind = Lean.Expr.const `Miri.Input.TypedEnumTag.borrowKind []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.fakeBorrowKind = Lean.Expr.const `Miri.Input.TypedEnumTag.fakeBorrowKind []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.mutBorrowKind = Lean.Expr.const `Miri.Input.TypedEnumTag.mutBorrowKind []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.mutability = Lean.Expr.const `Miri.Input.TypedEnumTag.mutability []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.castKind = Lean.Expr.const `Miri.Input.TypedEnumTag.castKind []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.pointerCoercion = Lean.Expr.const `Miri.Input.TypedEnumTag.pointerCoercion []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.coercionSource = Lean.Expr.const `Miri.Input.TypedEnumTag.coercionSource []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.unwindReason = Lean.Expr.const `Miri.Input.TypedEnumTag.unwindReason []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.aggregateKind = Lean.Expr.const `Miri.Input.TypedEnumTag.aggregateKind []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.unwindAction = Lean.Expr.const `Miri.Input.TypedEnumTag.unwindAction []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.mirPhase = Lean.Expr.const `Miri.Input.TypedEnumTag.mirPhase []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.mirPhaseStage = Lean.Expr.const `Miri.Input.TypedEnumTag.mirPhaseStage []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.withRetag = Lean.Expr.const `Miri.Input.TypedEnumTag.withRetag []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.runtimeCheck = Lean.Expr.const `Miri.Input.TypedEnumTag.runtimeCheck []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.fakeReadCause = Lean.Expr.const `Miri.Input.TypedEnumTag.fakeReadCause []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.callSource = Lean.Expr.const `Miri.Input.TypedEnumTag.callSource []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.backwardDropReason = Lean.Expr.const `Miri.Input.TypedEnumTag.backwardDropReason []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.regionKind = Lean.Expr.const `Miri.Input.TypedEnumTag.regionKind []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.boundRegionKind = Lean.Expr.const `Miri.Input.TypedEnumTag.boundRegionKind []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.boundVarIndexKind = Lean.Expr.const `Miri.Input.TypedEnumTag.boundVarIndexKind []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.lateParamRegionKind = Lean.Expr.const `Miri.Input.TypedEnumTag.lateParamRegionKind []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.integerType = Lean.Expr.const `Miri.Input.TypedEnumTag.integerType []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.floatType = Lean.Expr.const `Miri.Input.TypedEnumTag.floatType []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.adtKind = Lean.Expr.const `Miri.Input.TypedEnumTag.adtKind []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.variance = Lean.Expr.const `Miri.Input.TypedEnumTag.variance []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.coverageKind = Lean.Expr.const `Miri.Input.TypedEnumTag.coverageKind []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.coveragePointKind = Lean.Expr.const `Miri.Input.TypedEnumTag.coveragePointKind []
• Miri.Frontend.instToExprTypedEnumTag.toExpr Miri.Input.TypedEnumTag.fakeBorrowRetagMode = Lean.Expr.const `Miri.Input.TypedEnumTag.fakeBorrowRetagMode []
• Miri.Frontend.instToExprTypedEnumTag.toExpr (Miri.Input.TypedEnumTag.other a) = (Lean.Expr.const `Miri.Input.TypedEnumTag.other []).app (Lean.toExpr a)

def Miri.Frontend.instToExprUserTypeProjectionKind.toExpr : Input.UserTypeProjectionKind → Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Miri.Frontend.instToExprUserTypeProjectionKind.toExpr Miri.Input.UserTypeProjectionKind.deref = Lean.Expr.const `Miri.Input.UserTypeProjectionKind.deref []
• Miri.Frontend.instToExprUserTypeProjectionKind.toExpr (Miri.Input.UserTypeProjectionKind.field a) = (Lean.Expr.const `Miri.Input.UserTypeProjectionKind.field []).app (Lean.toExpr a)
• Miri.Frontend.instToExprUserTypeProjectionKind.toExpr Miri.Input.UserTypeProjectionKind.index = Lean.Expr.const `Miri.Input.UserTypeProjectionKind.index []
• Miri.Frontend.instToExprUserTypeProjectionKind.toExpr Miri.Input.UserTypeProjectionKind.opaqueCast = Lean.Expr.const `Miri.Input.UserTypeProjectionKind.opaqueCast []
• Miri.Frontend.instToExprUserTypeProjectionKind.toExpr Miri.Input.UserTypeProjectionKind.unwrapUnsafeBinder = Lean.Expr.const `Miri.Input.UserTypeProjectionKind.unwrapUnsafeBinder []
• Miri.Frontend.instToExprUserTypeProjectionKind.toExpr Miri.Input.UserTypeProjectionKind.phantomDeref = Lean.Expr.const `Miri.Input.UserTypeProjectionKind.phantomDeref []
• Miri.Frontend.instToExprUserTypeProjectionKind.toExpr (Miri.Input.UserTypeProjectionKind.unknown a) = (Lean.Expr.const `Miri.Input.UserTypeProjectionKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprUserTypeProjectionKind : Lean.ToExpr Input.UserTypeProjectionKind

Equations

• Miri.Frontend.instToExprUserTypeProjectionKind = { toExpr := Miri.Frontend.instToExprUserTypeProjectionKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.UserTypeProjectionKind [] }

def Miri.Frontend.instToExprUserTypeProjection.toExpr [Lean.ToExpr Lean.Json] : Input.UserTypeProjection → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprUserTypeProjection [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.UserTypeProjection

Equations

• Miri.Frontend.instToExprUserTypeProjection = { toExpr := Miri.Frontend.instToExprUserTypeProjection.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.UserTypeProjection [] }

def Miri.Frontend.instToExprFunctionSignature.toExpr [Lean.ToExpr Lean.Json] : Input.FunctionSignature → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprFunctionSignature [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.FunctionSignature

Equations

• Miri.Frontend.instToExprFunctionSignature = { toExpr := Miri.Frontend.instToExprFunctionSignature.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.FunctionSignature [] }

partial def Miri.Frontend.instToExprCompilerPattern.toExpr [Lean.ToExpr Lean.Json] : Input.CompilerPattern → Lean.Expr

@[instance_reducible]

instance Miri.Frontend.instToExprCompilerPattern [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.CompilerPattern

Equations

• Miri.Frontend.instToExprCompilerPattern = { toExpr := Miri.Frontend.instToExprCompilerPattern.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.CompilerPattern [] }

@[instance_reducible]

instance Miri.Frontend.instToExprCompilerBooleanEvidence [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.CompilerBooleanEvidence

Equations

• Miri.Frontend.instToExprCompilerBooleanEvidence = { toExpr := Miri.Frontend.instToExprCompilerBooleanEvidence.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.CompilerBooleanEvidence [] }

def Miri.Frontend.instToExprCompilerBooleanEvidence.toExpr [Lean.ToExpr Lean.Json] : Input.CompilerBooleanEvidence → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprCompilerTypeEvidence [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.CompilerTypeEvidence

Equations

• Miri.Frontend.instToExprCompilerTypeEvidence = { toExpr := Miri.Frontend.instToExprCompilerTypeEvidence.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.CompilerTypeEvidence [] }

def Miri.Frontend.instToExprCompilerTypeEvidence.toExpr [Lean.ToExpr Lean.Json] : Input.CompilerTypeEvidence → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprTypeCompilerFacts [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.TypeCompilerFacts

Equations

• Miri.Frontend.instToExprTypeCompilerFacts = { toExpr := Miri.Frontend.instToExprTypeCompilerFacts.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.TypeCompilerFacts [] }

def Miri.Frontend.instToExprTypeCompilerFacts.toExpr [Lean.ToExpr Lean.Json] : Input.TypeCompilerFacts → Lean.Expr

Equations

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

def Miri.Frontend.instToExprTypeNode.toExpr [Lean.ToExpr Lean.Json] : Input.TypeNode → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprTypeNode [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.TypeNode

Equations

• Miri.Frontend.instToExprTypeNode = { toExpr := Miri.Frontend.instToExprTypeNode.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.TypeNode [] }

def Miri.Frontend.instToExprInitRange.toExpr : Input.InitRange → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprInitRange : Lean.ToExpr Input.InitRange

Equations

• Miri.Frontend.instToExprInitRange = { toExpr := Miri.Frontend.instToExprInitRange.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.InitRange [] }

@[instance_reducible]

instance Miri.Frontend.instToExprRelocation : Lean.ToExpr Input.Relocation

Equations

• Miri.Frontend.instToExprRelocation = { toExpr := Miri.Frontend.instToExprRelocation.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.Relocation [] }

def Miri.Frontend.instToExprRelocation.toExpr : Input.Relocation → Lean.Expr

Equations

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

def Miri.Frontend.instToExprMemoryMutability.toExpr : Input.MemoryMutability → Lean.Expr

Equations

• Miri.Frontend.instToExprMemoryMutability.toExpr Miri.Input.MemoryMutability.mutable = Lean.Expr.const `Miri.Input.MemoryMutability.mutable []
• Miri.Frontend.instToExprMemoryMutability.toExpr Miri.Input.MemoryMutability.immutable = Lean.Expr.const `Miri.Input.MemoryMutability.immutable []
• Miri.Frontend.instToExprMemoryMutability.toExpr (Miri.Input.MemoryMutability.unknown a) = (Lean.Expr.const `Miri.Input.MemoryMutability.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprMemoryMutability : Lean.ToExpr Input.MemoryMutability

Equations

• Miri.Frontend.instToExprMemoryMutability = { toExpr := Miri.Frontend.instToExprMemoryMutability.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.MemoryMutability [] }

def Miri.Frontend.instToExprAllocationMemory.toExpr : Input.AllocationMemory → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprAllocationMemory : Lean.ToExpr Input.AllocationMemory

Equations

• Miri.Frontend.instToExprAllocationMemory = { toExpr := Miri.Frontend.instToExprAllocationMemory.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.AllocationMemory [] }

@[instance_reducible]

instance Miri.Frontend.instToExprAbiAttributes [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.AbiAttributes

Equations

• Miri.Frontend.instToExprAbiAttributes = { toExpr := Miri.Frontend.instToExprAbiAttributes.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.AbiAttributes [] }

def Miri.Frontend.instToExprAbiAttributes.toExpr [Lean.ToExpr Lean.Json] : Input.AbiAttributes → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprAbiRegisterKind : Lean.ToExpr Input.AbiRegisterKind

Equations

• Miri.Frontend.instToExprAbiRegisterKind = { toExpr := Miri.Frontend.instToExprAbiRegisterKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.AbiRegisterKind [] }

def Miri.Frontend.instToExprAbiRegisterKind.toExpr : Input.AbiRegisterKind → Lean.Expr

Equations

• Miri.Frontend.instToExprAbiRegisterKind.toExpr Miri.Input.AbiRegisterKind.integer = Lean.Expr.const `Miri.Input.AbiRegisterKind.integer []
• Miri.Frontend.instToExprAbiRegisterKind.toExpr Miri.Input.AbiRegisterKind.float = Lean.Expr.const `Miri.Input.AbiRegisterKind.float []
• Miri.Frontend.instToExprAbiRegisterKind.toExpr Miri.Input.AbiRegisterKind.ppcF128 = Lean.Expr.const `Miri.Input.AbiRegisterKind.ppcF128 []
• Miri.Frontend.instToExprAbiRegisterKind.toExpr Miri.Input.AbiRegisterKind.vector = Lean.Expr.const `Miri.Input.AbiRegisterKind.vector []
• Miri.Frontend.instToExprAbiRegisterKind.toExpr (Miri.Input.AbiRegisterKind.unknown a) = (Lean.Expr.const `Miri.Input.AbiRegisterKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprAbiRegister [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.AbiRegister

Equations

• Miri.Frontend.instToExprAbiRegister = { toExpr := Miri.Frontend.instToExprAbiRegister.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.AbiRegister [] }

def Miri.Frontend.instToExprAbiRegister.toExpr [Lean.ToExpr Lean.Json] : Input.AbiRegister → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprAbiCastTarget [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.AbiCastTarget

Equations

• Miri.Frontend.instToExprAbiCastTarget = { toExpr := Miri.Frontend.instToExprAbiCastTarget.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.AbiCastTarget [] }

def Miri.Frontend.instToExprAbiCastTarget.toExpr [Lean.ToExpr Lean.Json] : Input.AbiCastTarget → Lean.Expr

Equations

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

def Miri.Frontend.instToExprAbiPassMode.toExpr [Lean.ToExpr Lean.Json] : Input.AbiPassMode → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprAbiPassMode [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.AbiPassMode

Equations

• Miri.Frontend.instToExprAbiPassMode = { toExpr := Miri.Frontend.instToExprAbiPassMode.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.AbiPassMode [] }

def Miri.Frontend.instToExprAbiArgument.toExpr [Lean.ToExpr Lean.Json] : Input.AbiArgument → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprAbiArgument [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.AbiArgument

Equations

• Miri.Frontend.instToExprAbiArgument = { toExpr := Miri.Frontend.instToExprAbiArgument.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.AbiArgument [] }

def Miri.Frontend.instToExprFunctionAbi.toExpr [Lean.ToExpr Lean.Json] : Input.FunctionAbi → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprFunctionAbi [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.FunctionAbi

Equations

• Miri.Frontend.instToExprFunctionAbi = { toExpr := Miri.Frontend.instToExprFunctionAbi.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.FunctionAbi [] }

@[instance_reducible]

instance Miri.Frontend.instToExprTypedValue [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.TypedValue

Equations

• Miri.Frontend.instToExprTypedValue = { toExpr := Miri.Frontend.instToExprTypedValue.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.TypedValue [] }

partial def Miri.Frontend.instToExprTypedValue.toExpr [Lean.ToExpr Lean.Json] : Input.TypedValue → Lean.Expr

@[instance_reducible]

instance Miri.Frontend.instToExprDefinitionId : Lean.ToExpr Input.DefinitionId

Equations

• Miri.Frontend.instToExprDefinitionId = { toExpr := Miri.Frontend.instToExprDefinitionId.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.DefinitionId [] }

def Miri.Frontend.instToExprDefinitionId.toExpr : Input.DefinitionId → Lean.Expr

Equations

• Miri.Frontend.instToExprDefinitionId.toExpr { crateIndex := a, index := a_1 } = ((Lean.Expr.const `Miri.Input.DefinitionId.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

@[instance_reducible]

instance Miri.Frontend.instToExprVtableEntryKind : Lean.ToExpr Input.VtableEntryKind

Equations

• Miri.Frontend.instToExprVtableEntryKind = { toExpr := Miri.Frontend.instToExprVtableEntryKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.VtableEntryKind [] }

def Miri.Frontend.instToExprVtableEntryKind.toExpr : Input.VtableEntryKind → Lean.Expr

Equations

• Miri.Frontend.instToExprVtableEntryKind.toExpr Miri.Input.VtableEntryKind.dropInPlaceNull = Lean.Expr.const `Miri.Input.VtableEntryKind.dropInPlaceNull []
• Miri.Frontend.instToExprVtableEntryKind.toExpr Miri.Input.VtableEntryKind.dropInPlace = Lean.Expr.const `Miri.Input.VtableEntryKind.dropInPlace []
• Miri.Frontend.instToExprVtableEntryKind.toExpr Miri.Input.VtableEntryKind.sizeBytes = Lean.Expr.const `Miri.Input.VtableEntryKind.sizeBytes []
• Miri.Frontend.instToExprVtableEntryKind.toExpr Miri.Input.VtableEntryKind.alignBytes = Lean.Expr.const `Miri.Input.VtableEntryKind.alignBytes []
• Miri.Frontend.instToExprVtableEntryKind.toExpr Miri.Input.VtableEntryKind.vacant = Lean.Expr.const `Miri.Input.VtableEntryKind.vacant []
• Miri.Frontend.instToExprVtableEntryKind.toExpr Miri.Input.VtableEntryKind.method = Lean.Expr.const `Miri.Input.VtableEntryKind.method []
• Miri.Frontend.instToExprVtableEntryKind.toExpr Miri.Input.VtableEntryKind.supertraitVtablePointer = Lean.Expr.const `Miri.Input.VtableEntryKind.supertraitVtablePointer []
• Miri.Frontend.instToExprVtableEntryKind.toExpr (Miri.Input.VtableEntryKind.unknown a) = (Lean.Expr.const `Miri.Input.VtableEntryKind.unknown []).app (Lean.toExpr a)

def Miri.Frontend.instToExprVtablePredicateKind.toExpr : Input.VtablePredicateKind → Lean.Expr

Equations

• Miri.Frontend.instToExprVtablePredicateKind.toExpr Miri.Input.VtablePredicateKind.trait = Lean.Expr.const `Miri.Input.VtablePredicateKind.trait []
• Miri.Frontend.instToExprVtablePredicateKind.toExpr Miri.Input.VtablePredicateKind.autoTrait = Lean.Expr.const `Miri.Input.VtablePredicateKind.autoTrait []
• Miri.Frontend.instToExprVtablePredicateKind.toExpr Miri.Input.VtablePredicateKind.projection = Lean.Expr.const `Miri.Input.VtablePredicateKind.projection []
• Miri.Frontend.instToExprVtablePredicateKind.toExpr (Miri.Input.VtablePredicateKind.unknown a) = (Lean.Expr.const `Miri.Input.VtablePredicateKind.unknown []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprVtablePredicateKind : Lean.ToExpr Input.VtablePredicateKind

Equations

• Miri.Frontend.instToExprVtablePredicateKind = { toExpr := Miri.Frontend.instToExprVtablePredicateKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.VtablePredicateKind [] }

@[instance_reducible]

instance Miri.Frontend.instToExprFunctionAllocation [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.FunctionAllocation

Equations

• Miri.Frontend.instToExprFunctionAllocation = { toExpr := Miri.Frontend.instToExprFunctionAllocation.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.FunctionAllocation [] }

def Miri.Frontend.instToExprFunctionAllocation.toExpr [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Input.FunctionAllocation → Lean.Expr

Equations

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

def Miri.Frontend.instToExprStaticGlobalInfo.toExpr [Lean.ToExpr Lean.Json] : Input.StaticGlobalInfo → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprStaticGlobalInfo [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.StaticGlobalInfo

Equations

• Miri.Frontend.instToExprStaticGlobalInfo = { toExpr := Miri.Frontend.instToExprStaticGlobalInfo.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.StaticGlobalInfo [] }

def Miri.Frontend.instToExprStaticAllocation.toExpr [Lean.ToExpr Lean.Json] : Input.StaticAllocation → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprStaticAllocation [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.StaticAllocation

Equations

• Miri.Frontend.instToExprStaticAllocation = { toExpr := Miri.Frontend.instToExprStaticAllocation.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.StaticAllocation [] }

def Miri.Frontend.instToExprVtablePredicate.toExpr [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Input.VtablePredicate → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprVtablePredicate [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.VtablePredicate

Equations

• Miri.Frontend.instToExprVtablePredicate = { toExpr := Miri.Frontend.instToExprVtablePredicate.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.VtablePredicate [] }

@[instance_reducible]

instance Miri.Frontend.instToExprVtableEntry [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.VtableEntry

Equations

• Miri.Frontend.instToExprVtableEntry = { toExpr := Miri.Frontend.instToExprVtableEntry.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.VtableEntry [] }

def Miri.Frontend.instToExprVtableEntry.toExpr [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Input.VtableEntry → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprVtableAllocation [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.VtableAllocation

Equations

• Miri.Frontend.instToExprVtableAllocation = { toExpr := Miri.Frontend.instToExprVtableAllocation.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.VtableAllocation [] }

def Miri.Frontend.instToExprVtableAllocation.toExpr [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Input.VtableAllocation → Lean.Expr

Equations

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

def Miri.Frontend.instToExprAllocationData.toExpr [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Input.AllocationData → Lean.Expr

Equations

• Miri.Frontend.instToExprAllocationData.toExpr (Miri.Input.AllocationData.memory a) = (Lean.Expr.const `Miri.Input.AllocationData.memory []).app (Lean.toExpr a)
• Miri.Frontend.instToExprAllocationData.toExpr (Miri.Input.AllocationData.function a) = (Lean.Expr.const `Miri.Input.AllocationData.function []).app (Lean.toExpr a)
• Miri.Frontend.instToExprAllocationData.toExpr (Miri.Input.AllocationData.static a) = (Lean.Expr.const `Miri.Input.AllocationData.static []).app (Lean.toExpr a)
• Miri.Frontend.instToExprAllocationData.toExpr (Miri.Input.AllocationData.vtable a) = (Lean.Expr.const `Miri.Input.AllocationData.vtable []).app (Lean.toExpr a)
• Miri.Frontend.instToExprAllocationData.toExpr (Miri.Input.AllocationData.typeId a) = (Lean.Expr.const `Miri.Input.AllocationData.typeId []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprAllocationData [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.AllocationData

Equations

• Miri.Frontend.instToExprAllocationData = { toExpr := Miri.Frontend.instToExprAllocationData.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.AllocationData [] }

def Miri.Frontend.instToExprAllocationNode.toExpr [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Input.AllocationNode → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprAllocationNode [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.AllocationNode

Equations

• Miri.Frontend.instToExprAllocationNode = { toExpr := Miri.Frontend.instToExprAllocationNode.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.AllocationNode [] }

def Miri.Frontend.instToExprMirNode.toExpr [Lean.ToExpr Input.TypedValue] : Input.MirNode → Lean.Expr

Equations

• Miri.Frontend.instToExprMirNode.toExpr { value := a, sourceInfo := a_1 } = ((Lean.Expr.const `Miri.Input.MirNode.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

@[instance_reducible]

instance Miri.Frontend.instToExprMirNode [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.MirNode

Equations

• Miri.Frontend.instToExprMirNode = { toExpr := Miri.Frontend.instToExprMirNode.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.MirNode [] }

@[instance_reducible]

instance Miri.Frontend.instToExprBasicBlock [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.BasicBlock

Equations

• Miri.Frontend.instToExprBasicBlock = { toExpr := Miri.Frontend.instToExprBasicBlock.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.BasicBlock [] }

def Miri.Frontend.instToExprBasicBlock.toExpr [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Input.BasicBlock → Lean.Expr

Equations

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

def Miri.Frontend.instToExprLocalDecl.toExpr [Lean.ToExpr Lean.Json] : Input.LocalDecl → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprLocalDecl [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.LocalDecl

Equations

• Miri.Frontend.instToExprLocalDecl = { toExpr := Miri.Frontend.instToExprLocalDecl.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.LocalDecl [] }

def Miri.Frontend.instToExprBodyCore.toExpr [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Input.BodyCore → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprBodyCore [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.BodyCore

Equations

• Miri.Frontend.instToExprBodyCore = { toExpr := Miri.Frontend.instToExprBodyCore.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.BodyCore [] }

def Miri.Frontend.instToExprPromotedBody.toExpr [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Input.PromotedBody → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprPromotedBody [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.PromotedBody

Equations

• Miri.Frontend.instToExprPromotedBody = { toExpr := Miri.Frontend.instToExprPromotedBody.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.PromotedBody [] }

def Miri.Frontend.instToExprBody.toExpr [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Input.Body → Lean.Expr

Equations

• Miri.Frontend.instToExprBody.toExpr { toBodyCore := a, promotedBodies := a_1 } = ((Lean.Expr.const `Miri.Input.Body.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

@[instance_reducible]

instance Miri.Frontend.instToExprBody [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.Body

Equations

• Miri.Frontend.instToExprBody = { toExpr := Miri.Frontend.instToExprBody.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.Body [] }

@[instance_reducible]

instance Miri.Frontend.instToExprInstanceNode [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.InstanceNode

Equations

• Miri.Frontend.instToExprInstanceNode = { toExpr := Miri.Frontend.instToExprInstanceNode.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.InstanceNode [] }

def Miri.Frontend.instToExprInstanceNode.toExpr [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Input.InstanceNode → Lean.Expr

Equations

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

def Miri.Frontend.instToExprScopeRoot.toExpr : Input.ScopeRoot → Lean.Expr

Equations

• Miri.Frontend.instToExprScopeRoot.toExpr { defPath := a, definitionId := a_1 } = ((Lean.Expr.const `Miri.Input.ScopeRoot.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

@[instance_reducible]

instance Miri.Frontend.instToExprScopeRoot : Lean.ToExpr Input.ScopeRoot

Equations

• Miri.Frontend.instToExprScopeRoot = { toExpr := Miri.Frontend.instToExprScopeRoot.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.ScopeRoot [] }

@[instance_reducible]

instance Miri.Frontend.instToExprSelectedScope [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.SelectedScope

Equations

• Miri.Frontend.instToExprSelectedScope = { toExpr := Miri.Frontend.instToExprSelectedScope.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.SelectedScope [] }

def Miri.Frontend.instToExprSelectedScope.toExpr [Lean.ToExpr Lean.Json] : Input.SelectedScope → Lean.Expr

Equations

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

def Miri.Frontend.instToExprTargetDataLayoutEvidence.toExpr [Lean.ToExpr Lean.Json] : Input.TargetDataLayoutEvidence → Lean.Expr

Equations

• Miri.Frontend.instToExprTargetDataLayoutEvidence.toExpr { status := a, payload := a_1 } = ((Lean.Expr.const `Miri.Input.TargetDataLayoutEvidence.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

@[instance_reducible]

instance Miri.Frontend.instToExprTargetDataLayoutEvidence [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.TargetDataLayoutEvidence

Equations

• Miri.Frontend.instToExprTargetDataLayoutEvidence = { toExpr := Miri.Frontend.instToExprTargetDataLayoutEvidence.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.TargetDataLayoutEvidence [] }

@[instance_reducible]

instance Miri.Frontend.instToExprCompilerPredicateEvidence [Lean.ToExpr Lean.Json] : Lean.ToExpr Input.CompilerPredicateEvidence

Equations

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

def Miri.Frontend.instToExprCompilerPredicateEvidence.toExpr [Lean.ToExpr Lean.Json] : Input.CompilerPredicateEvidence → Lean.Expr

Equations

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

def Miri.Frontend.instToExprSourceAllocIdKind.toExpr : Input.SourceAllocIdKind → Lean.Expr

Equations

• Miri.Frontend.instToExprSourceAllocIdKind.toExpr Miri.Input.SourceAllocIdKind.dangling = Lean.Expr.const `Miri.Input.SourceAllocIdKind.dangling []
• Miri.Frontend.instToExprSourceAllocIdKind.toExpr Miri.Input.SourceAllocIdKind.memory = Lean.Expr.const `Miri.Input.SourceAllocIdKind.memory []
• Miri.Frontend.instToExprSourceAllocIdKind.toExpr Miri.Input.SourceAllocIdKind.function = Lean.Expr.const `Miri.Input.SourceAllocIdKind.function []
• Miri.Frontend.instToExprSourceAllocIdKind.toExpr Miri.Input.SourceAllocIdKind.vtable = Lean.Expr.const `Miri.Input.SourceAllocIdKind.vtable []
• Miri.Frontend.instToExprSourceAllocIdKind.toExpr Miri.Input.SourceAllocIdKind.static = Lean.Expr.const `Miri.Input.SourceAllocIdKind.static []
• Miri.Frontend.instToExprSourceAllocIdKind.toExpr Miri.Input.SourceAllocIdKind.typeId = Lean.Expr.const `Miri.Input.SourceAllocIdKind.typeId []

@[instance_reducible]

instance Miri.Frontend.instToExprSourceAllocIdKind : Lean.ToExpr Input.SourceAllocIdKind

Equations

• Miri.Frontend.instToExprSourceAllocIdKind = { toExpr := Miri.Frontend.instToExprSourceAllocIdKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.SourceAllocIdKind [] }

def Miri.Frontend.instToExprSourceAllocIdStatus.toExpr : Input.SourceAllocIdStatus → Lean.Expr

Equations

• Miri.Frontend.instToExprSourceAllocIdStatus.toExpr Miri.Input.SourceAllocIdStatus.dangling = Lean.Expr.const `Miri.Input.SourceAllocIdStatus.dangling []
• Miri.Frontend.instToExprSourceAllocIdStatus.toExpr Miri.Input.SourceAllocIdStatus.serialized = Lean.Expr.const `Miri.Input.SourceAllocIdStatus.serialized []
• Miri.Frontend.instToExprSourceAllocIdStatus.toExpr Miri.Input.SourceAllocIdStatus.opaque = Lean.Expr.const `Miri.Input.SourceAllocIdStatus.opaque []

@[instance_reducible]

instance Miri.Frontend.instToExprSourceAllocIdStatus : Lean.ToExpr Input.SourceAllocIdStatus

Equations

• Miri.Frontend.instToExprSourceAllocIdStatus = { toExpr := Miri.Frontend.instToExprSourceAllocIdStatus.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.SourceAllocIdStatus [] }

def Miri.Frontend.instToExprSourceAllocIdPoolRow.toExpr : Input.SourceAllocIdPoolRow → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprSourceAllocIdPoolRow : Lean.ToExpr Input.SourceAllocIdPoolRow

Equations

• Miri.Frontend.instToExprSourceAllocIdPoolRow = { toExpr := Miri.Frontend.instToExprSourceAllocIdPoolRow.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.SourceAllocIdPoolRow [] }

def Miri.Frontend.instToExprSourceAllocIdDedupKind.toExpr : Input.SourceAllocIdDedupKind → Lean.Expr

Equations

• Miri.Frontend.instToExprSourceAllocIdDedupKind.toExpr Miri.Input.SourceAllocIdDedupKind.function = Lean.Expr.const `Miri.Input.SourceAllocIdDedupKind.function []
• Miri.Frontend.instToExprSourceAllocIdDedupKind.toExpr Miri.Input.SourceAllocIdDedupKind.vtable = Lean.Expr.const `Miri.Input.SourceAllocIdDedupKind.vtable []
• Miri.Frontend.instToExprSourceAllocIdDedupKind.toExpr Miri.Input.SourceAllocIdDedupKind.static = Lean.Expr.const `Miri.Input.SourceAllocIdDedupKind.static []
• Miri.Frontend.instToExprSourceAllocIdDedupKind.toExpr Miri.Input.SourceAllocIdDedupKind.typeId = Lean.Expr.const `Miri.Input.SourceAllocIdDedupKind.typeId []
• Miri.Frontend.instToExprSourceAllocIdDedupKind.toExpr Miri.Input.SourceAllocIdDedupKind.memory = Lean.Expr.const `Miri.Input.SourceAllocIdDedupKind.memory []
• Miri.Frontend.instToExprSourceAllocIdDedupKind.toExpr Miri.Input.SourceAllocIdDedupKind.bytes = Lean.Expr.const `Miri.Input.SourceAllocIdDedupKind.bytes []

@[instance_reducible]

instance Miri.Frontend.instToExprSourceAllocIdDedupKind : Lean.ToExpr Input.SourceAllocIdDedupKind

Equations

• Miri.Frontend.instToExprSourceAllocIdDedupKind = { toExpr := Miri.Frontend.instToExprSourceAllocIdDedupKind.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.SourceAllocIdDedupKind [] }

def Miri.Frontend.instToExprSourceAllocIdProbeOutcome.toExpr : Input.SourceAllocIdProbeOutcome → Lean.Expr

Equations

• Miri.Frontend.instToExprSourceAllocIdProbeOutcome.toExpr Miri.Input.SourceAllocIdProbeOutcome.preexistingHit = Lean.Expr.const `Miri.Input.SourceAllocIdProbeOutcome.preexistingHit []
• Miri.Frontend.instToExprSourceAllocIdProbeOutcome.toExpr Miri.Input.SourceAllocIdProbeOutcome.missReservedByProbe = Lean.Expr.const `Miri.Input.SourceAllocIdProbeOutcome.missReservedByProbe []

@[instance_reducible]

instance Miri.Frontend.instToExprSourceAllocIdProbeOutcome : Lean.ToExpr Input.SourceAllocIdProbeOutcome

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprSourceAllocIdSaltResult : Lean.ToExpr Input.SourceAllocIdSaltResult

Equations

• Miri.Frontend.instToExprSourceAllocIdSaltResult = { toExpr := Miri.Frontend.instToExprSourceAllocIdSaltResult.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.SourceAllocIdSaltResult [] }

def Miri.Frontend.instToExprSourceAllocIdSaltResult.toExpr : Input.SourceAllocIdSaltResult → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprSourceAllocIdDedupRow : Lean.ToExpr Input.SourceAllocIdDedupRow

Equations

• Miri.Frontend.instToExprSourceAllocIdDedupRow = { toExpr := Miri.Frontend.instToExprSourceAllocIdDedupRow.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.SourceAllocIdDedupRow [] }

def Miri.Frontend.instToExprSourceAllocIdDedupRow.toExpr : Input.SourceAllocIdDedupRow → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprCompilerAllocIdWorld : Lean.ToExpr Input.CompilerAllocIdWorld

Equations

• Miri.Frontend.instToExprCompilerAllocIdWorld = { toExpr := Miri.Frontend.instToExprCompilerAllocIdWorld.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.CompilerAllocIdWorld [] }

def Miri.Frontend.instToExprCompilerAllocIdWorld.toExpr : Input.CompilerAllocIdWorld → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprImportDocument [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.ImportDocument

Equations

• Miri.Frontend.instToExprImportDocument = { toExpr := Miri.Frontend.instToExprImportDocument.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.ImportDocument [] }

def Miri.Frontend.instToExprImportDocument.toExpr [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Input.ImportDocument → Lean.Expr

Equations

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

def Miri.Frontend.instToExprExecutionInput.toExpr [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Input.ExecutionInput → Lean.Expr

Equations

• Miri.Frontend.instToExprExecutionInput.toExpr { document := a } = (Lean.Expr.const `Miri.Input.ExecutionInput.mk []).app (Lean.toExpr a)

@[instance_reducible]

instance Miri.Frontend.instToExprExecutionInput [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.ExecutionInput

Equations

• Miri.Frontend.instToExprExecutionInput = { toExpr := Miri.Frontend.instToExprExecutionInput.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.ExecutionInput [] }

def Miri.Frontend.instToExprDecodeResult.toExpr [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Input.DecodeResult → Lean.Expr

Equations

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

@[instance_reducible]

instance Miri.Frontend.instToExprDecodeResult [Lean.ToExpr Lean.Json] [Lean.ToExpr Input.TypedValue] : Lean.ToExpr Input.DecodeResult

Equations

• Miri.Frontend.instToExprDecodeResult = { toExpr := Miri.Frontend.instToExprDecodeResult.toExpr, toTypeExpr := Lean.Expr.const `Miri.Input.DecodeResult [] }

def Miri.Frontend.importMir : Lean.ParserDescr

Import a decoded document as a closed, kernel-checked Lean value. executionInput records structural readiness only. Unsupported semantics stay in the document's obligations; this command never produces a safety theorem.

Equations

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