Pinned, typed mirror of the MIR syntax datatypes used by the interpreter.

This module contains data constructors only; it does not claim that Lean has implemented their operational semantics. In particular, decoder failures and unsupported execution features belong in the Input layer as obligations, never as an executable "other" constructor here. Compiler-owned values (types, definition identities, spans, regions and generic constants) use explicit IDs or typed records; no JSON object or tag/string dispatch is part of this AST.

Stable references for compiler graph nodes. These are compilation-local and must be resolved against the corresponding typed metadata tables before execution.

@[reducible, inline]

abbrev Miri.MIR.TyId : Type

Equations

• Miri.MIR.TyId = Nat

@[reducible, inline]

abbrev Miri.MIR.DefId : Type

Equations

• Miri.MIR.DefId = Nat

@[reducible, inline]

abbrev Miri.MIR.LocalId : Type

Equations

• Miri.MIR.LocalId = Nat

@[reducible, inline]

abbrev Miri.MIR.BasicBlockId : Type

Equations

• Miri.MIR.BasicBlockId = Nat

@[reducible, inline]

abbrev Miri.MIR.AllocationId : Type

Equations

• Miri.MIR.AllocationId = Nat

@[reducible, inline]

abbrev Miri.MIR.TypeConstId : Type

Equations

• Miri.MIR.TypeConstId = Nat

@[reducible, inline]

abbrev Miri.MIR.SpanId : Type

Equations

• Miri.MIR.SpanId = Nat

@[reducible, inline]

abbrev Miri.MIR.FieldIndex : Type

Equations

• Miri.MIR.FieldIndex = Nat

@[reducible, inline]

abbrev Miri.MIR.VariantIndex : Type

Equations

• Miri.MIR.VariantIndex = Nat

@[reducible, inline]

abbrev Miri.MIR.UserTypeAnnotationIndex : Type

Equations

• Miri.MIR.UserTypeAnnotationIndex = Nat

@[reducible, inline]

abbrev Miri.MIR.HirOwnerId : Type

Equations

• Miri.MIR.HirOwnerId = Nat

@[reducible, inline]

abbrev Miri.MIR.HirLocalId : Type

Equations

• Miri.MIR.HirLocalId = Nat

Source MIR locations identify the start of a statement, or the terminator when statementIndex equals that block's statement count.

structure Miri.MIR.Location : Type

• block : BasicBlockId
• statementIndex : Nat

def Miri.MIR.instReprLocation.repr : Location → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprLocation : Repr Location

Equations

• Miri.MIR.instReprLocation = { reprPrec := Miri.MIR.instReprLocation.repr }

def Miri.MIR.instDecidableEqLocation.decEq (x✝ x✝¹ : Location) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqLocation : DecidableEq Location

Equations

• Miri.MIR.instDecidableEqLocation = Miri.MIR.instDecidableEqLocation.decEq

def Miri.MIR.Location.start : Location

Equations

• Miri.MIR.Location.start = { block := 0, statementIndex := 0 }

def Miri.MIR.Location.successorWithinBlock (location : Location) : Location

Equations

• location.successorWithinBlock = { block := location.block, statementIndex := location.statementIndex + 1 }

structure Miri.MIR.SpanRef : Type

• id : SpanId

def Miri.MIR.instReprSpanRef.repr : SpanRef → Nat → Std.Format

Equations

• Miri.MIR.instReprSpanRef.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "id" ++ Std.Format.text " := " ++ (Std.Format.nest 6 (repr x✝.id)).group) " }"

@[instance_reducible]

instance Miri.MIR.instReprSpanRef : Repr SpanRef

Equations

• Miri.MIR.instReprSpanRef = { reprPrec := Miri.MIR.instReprSpanRef.repr }

def Miri.MIR.instDecidableEqSpanRef.decEq (x✝ x✝¹ : SpanRef) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqSpanRef.decEq { id := a } { id := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqSpanRef : DecidableEq SpanRef

Equations

• Miri.MIR.instDecidableEqSpanRef = Miri.MIR.instDecidableEqSpanRef.decEq

inductive Miri.MIR.Mutability : Type

• Not : Mutability
• Mut : Mutability

def Miri.MIR.instReprMutability.repr : Mutability → Nat → Std.Format

Equations

• Miri.MIR.instReprMutability.repr Miri.MIR.Mutability.Not prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.Mutability.Not")).group prec✝
• Miri.MIR.instReprMutability.repr Miri.MIR.Mutability.Mut prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.Mutability.Mut")).group prec✝

@[instance_reducible]

instance Miri.MIR.instReprMutability : Repr Mutability

Equations

• Miri.MIR.instReprMutability = { reprPrec := Miri.MIR.instReprMutability.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqMutability : DecidableEq Mutability

Equations

• Miri.MIR.instDecidableEqMutability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.Safety : Type

• Safe : Safety
• Unsafe : Safety

@[instance_reducible]

instance Miri.MIR.instReprSafety : Repr Safety

Equations

• Miri.MIR.instReprSafety = { reprPrec := Miri.MIR.instReprSafety.repr }

def Miri.MIR.instReprSafety.repr : Safety → Nat → Std.Format

Equations

• Miri.MIR.instReprSafety.repr Miri.MIR.Safety.Safe prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.Safety.Safe")).group prec✝
• Miri.MIR.instReprSafety.repr Miri.MIR.Safety.Unsafe prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.Safety.Unsafe")).group prec✝

@[instance_reducible]

instance Miri.MIR.instDecidableEqSafety : DecidableEq Safety

Equations

• Miri.MIR.instDecidableEqSafety x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.Variance : Type

• Covariant : Variance
• Contravariant : Variance
• Invariant : Variance
• Bivariant : Variance

def Miri.MIR.instReprVariance.repr : Variance → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instReprVariance.repr Miri.MIR.Variance.Covariant prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.Variance.Covariant")).group prec✝
• Miri.MIR.instReprVariance.repr Miri.MIR.Variance.Invariant prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.Variance.Invariant")).group prec✝
• Miri.MIR.instReprVariance.repr Miri.MIR.Variance.Bivariant prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.Variance.Bivariant")).group prec✝

@[instance_reducible]

instance Miri.MIR.instReprVariance : Repr Variance

Equations

• Miri.MIR.instReprVariance = { reprPrec := Miri.MIR.instReprVariance.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqVariance : DecidableEq Variance

Equations

• Miri.MIR.instDecidableEqVariance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.PointerCoercion : Type

• ReifyFnPointer (safety : Safety) : PointerCoercion
• UnsafeFnPointer : PointerCoercion
• ClosureFnPointer (safety : Safety) : PointerCoercion
• MutToConstPointer : PointerCoercion
• ArrayToPointer : PointerCoercion
• Unsize : PointerCoercion

def Miri.MIR.instReprPointerCoercion.repr : PointerCoercion → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprPointerCoercion : Repr PointerCoercion

Equations

• Miri.MIR.instReprPointerCoercion = { reprPrec := Miri.MIR.instReprPointerCoercion.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqPointerCoercion : DecidableEq PointerCoercion

Equations

• Miri.MIR.instDecidableEqPointerCoercion = Miri.MIR.instDecidableEqPointerCoercion.decEq

def Miri.MIR.instDecidableEqPointerCoercion.decEq (x✝ x✝¹ : PointerCoercion) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqPointerCoercion.decEq (Miri.MIR.PointerCoercion.ReifyFnPointer a) (Miri.MIR.PointerCoercion.ReifyFnPointer b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq (Miri.MIR.PointerCoercion.ReifyFnPointer safety) Miri.MIR.PointerCoercion.UnsafeFnPointer = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq (Miri.MIR.PointerCoercion.ReifyFnPointer safety) (Miri.MIR.PointerCoercion.ClosureFnPointer safety_1) = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq (Miri.MIR.PointerCoercion.ReifyFnPointer safety) Miri.MIR.PointerCoercion.MutToConstPointer = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq (Miri.MIR.PointerCoercion.ReifyFnPointer safety) Miri.MIR.PointerCoercion.ArrayToPointer = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq (Miri.MIR.PointerCoercion.ReifyFnPointer safety) Miri.MIR.PointerCoercion.Unsize = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.UnsafeFnPointer (Miri.MIR.PointerCoercion.ReifyFnPointer safety) = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.UnsafeFnPointer Miri.MIR.PointerCoercion.UnsafeFnPointer = isTrue ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.UnsafeFnPointer (Miri.MIR.PointerCoercion.ClosureFnPointer safety) = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.UnsafeFnPointer Miri.MIR.PointerCoercion.ArrayToPointer = isFalse Miri.MIR.instDecidableEqPointerCoercion.decEq._proof_11
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.UnsafeFnPointer Miri.MIR.PointerCoercion.Unsize = isFalse Miri.MIR.instDecidableEqPointerCoercion.decEq._proof_12
• Miri.MIR.instDecidableEqPointerCoercion.decEq (Miri.MIR.PointerCoercion.ClosureFnPointer safety) (Miri.MIR.PointerCoercion.ReifyFnPointer safety_1) = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq (Miri.MIR.PointerCoercion.ClosureFnPointer safety) Miri.MIR.PointerCoercion.UnsafeFnPointer = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq (Miri.MIR.PointerCoercion.ClosureFnPointer a) (Miri.MIR.PointerCoercion.ClosureFnPointer b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq (Miri.MIR.PointerCoercion.ClosureFnPointer safety) Miri.MIR.PointerCoercion.MutToConstPointer = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq (Miri.MIR.PointerCoercion.ClosureFnPointer safety) Miri.MIR.PointerCoercion.ArrayToPointer = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq (Miri.MIR.PointerCoercion.ClosureFnPointer safety) Miri.MIR.PointerCoercion.Unsize = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.MutToConstPointer (Miri.MIR.PointerCoercion.ReifyFnPointer safety) = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.MutToConstPointer (Miri.MIR.PointerCoercion.ClosureFnPointer safety) = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.MutToConstPointer Miri.MIR.PointerCoercion.MutToConstPointer = isTrue ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.MutToConstPointer Miri.MIR.PointerCoercion.Unsize = isFalse Miri.MIR.instDecidableEqPointerCoercion.decEq._proof_24
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.ArrayToPointer (Miri.MIR.PointerCoercion.ReifyFnPointer safety) = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.ArrayToPointer Miri.MIR.PointerCoercion.UnsafeFnPointer = isFalse Miri.MIR.instDecidableEqPointerCoercion.decEq._proof_26
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.ArrayToPointer (Miri.MIR.PointerCoercion.ClosureFnPointer safety) = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.ArrayToPointer Miri.MIR.PointerCoercion.ArrayToPointer = isTrue ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.ArrayToPointer Miri.MIR.PointerCoercion.Unsize = isFalse Miri.MIR.instDecidableEqPointerCoercion.decEq._proof_29
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.Unsize (Miri.MIR.PointerCoercion.ReifyFnPointer safety) = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.Unsize Miri.MIR.PointerCoercion.UnsafeFnPointer = isFalse Miri.MIR.instDecidableEqPointerCoercion.decEq._proof_31
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.Unsize (Miri.MIR.PointerCoercion.ClosureFnPointer safety) = isFalse ⋯
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.Unsize Miri.MIR.PointerCoercion.MutToConstPointer = isFalse Miri.MIR.instDecidableEqPointerCoercion.decEq._proof_33
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.Unsize Miri.MIR.PointerCoercion.ArrayToPointer = isFalse Miri.MIR.instDecidableEqPointerCoercion.decEq._proof_34
• Miri.MIR.instDecidableEqPointerCoercion.decEq Miri.MIR.PointerCoercion.Unsize Miri.MIR.PointerCoercion.Unsize = isTrue ⋯

inductive Miri.MIR.CoercionSource : Type

• AsCast : CoercionSource
• Implicit : CoercionSource

def Miri.MIR.instReprCoercionSource.repr : CoercionSource → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprCoercionSource : Repr CoercionSource

Equations

• Miri.MIR.instReprCoercionSource = { reprPrec := Miri.MIR.instReprCoercionSource.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqCoercionSource : DecidableEq CoercionSource

Equations

• Miri.MIR.instDecidableEqCoercionSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.CastKind : Type

• PointerExposeProvenance : CastKind
• PointerWithExposedProvenance : CastKind
• PointerCoercion (coercion : MIR.PointerCoercion) (source : CoercionSource) : CastKind
• IntToInt : CastKind
• FloatToInt : CastKind
• FloatToFloat : CastKind
• IntToFloat : CastKind
• PtrToPtr : CastKind
• FnPtrToPtr : CastKind
• Transmute : CastKind
• BoxDerefTransmute : CastKind
• Subtype : CastKind

def Miri.MIR.instReprCastKind.repr : CastKind → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instReprCastKind.repr Miri.MIR.CastKind.IntToInt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.CastKind.IntToInt")).group prec✝
• Miri.MIR.instReprCastKind.repr Miri.MIR.CastKind.PtrToPtr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.CastKind.PtrToPtr")).group prec✝
• Miri.MIR.instReprCastKind.repr Miri.MIR.CastKind.Transmute prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.CastKind.Transmute")).group prec✝
• Miri.MIR.instReprCastKind.repr Miri.MIR.CastKind.Subtype prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.CastKind.Subtype")).group prec✝

@[instance_reducible]

instance Miri.MIR.instReprCastKind : Repr CastKind

Equations

• Miri.MIR.instReprCastKind = { reprPrec := Miri.MIR.instReprCastKind.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqCastKind : DecidableEq CastKind

Equations

• Miri.MIR.instDecidableEqCastKind = Miri.MIR.instDecidableEqCastKind.decEq

def Miri.MIR.instDecidableEqCastKind.decEq (x✝ x✝¹ : CastKind) : Decidable (x✝ = x✝¹)

Equations

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

inductive Miri.MIR.FakeBorrowKind : Type

• Shallow : FakeBorrowKind
• Deep : FakeBorrowKind

def Miri.MIR.instReprFakeBorrowKind.repr : FakeBorrowKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprFakeBorrowKind : Repr FakeBorrowKind

Equations

• Miri.MIR.instReprFakeBorrowKind = { reprPrec := Miri.MIR.instReprFakeBorrowKind.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqFakeBorrowKind : DecidableEq FakeBorrowKind

Equations

• Miri.MIR.instDecidableEqFakeBorrowKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.MutBorrowKind : Type

• Default : MutBorrowKind
• TwoPhaseBorrow : MutBorrowKind
• ClosureCapture : MutBorrowKind

@[instance_reducible]

instance Miri.MIR.instReprMutBorrowKind : Repr MutBorrowKind

Equations

• Miri.MIR.instReprMutBorrowKind = { reprPrec := Miri.MIR.instReprMutBorrowKind.repr }

def Miri.MIR.instReprMutBorrowKind.repr : MutBorrowKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqMutBorrowKind : DecidableEq MutBorrowKind

Equations

• Miri.MIR.instDecidableEqMutBorrowKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.BorrowKind : Type

• Shared : BorrowKind
• Fake (kind : FakeBorrowKind) : BorrowKind
• Mut (kind : MutBorrowKind) : BorrowKind

@[instance_reducible]

instance Miri.MIR.instReprBorrowKind : Repr BorrowKind

Equations

• Miri.MIR.instReprBorrowKind = { reprPrec := Miri.MIR.instReprBorrowKind.repr }

def Miri.MIR.instReprBorrowKind.repr : BorrowKind → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instReprBorrowKind.repr Miri.MIR.BorrowKind.Shared prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BorrowKind.Shared")).group prec✝

@[instance_reducible]

instance Miri.MIR.instDecidableEqBorrowKind : DecidableEq BorrowKind

Equations

• Miri.MIR.instDecidableEqBorrowKind = Miri.MIR.instDecidableEqBorrowKind.decEq

def Miri.MIR.instDecidableEqBorrowKind.decEq (x✝ x✝¹ : BorrowKind) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqBorrowKind.decEq Miri.MIR.BorrowKind.Shared Miri.MIR.BorrowKind.Shared = isTrue ⋯
• Miri.MIR.instDecidableEqBorrowKind.decEq Miri.MIR.BorrowKind.Shared (Miri.MIR.BorrowKind.Fake kind) = isFalse ⋯
• Miri.MIR.instDecidableEqBorrowKind.decEq Miri.MIR.BorrowKind.Shared (Miri.MIR.BorrowKind.Mut kind) = isFalse ⋯
• Miri.MIR.instDecidableEqBorrowKind.decEq (Miri.MIR.BorrowKind.Fake kind) Miri.MIR.BorrowKind.Shared = isFalse ⋯
• Miri.MIR.instDecidableEqBorrowKind.decEq (Miri.MIR.BorrowKind.Fake a) (Miri.MIR.BorrowKind.Fake b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqBorrowKind.decEq (Miri.MIR.BorrowKind.Fake kind) (Miri.MIR.BorrowKind.Mut kind_1) = isFalse ⋯
• Miri.MIR.instDecidableEqBorrowKind.decEq (Miri.MIR.BorrowKind.Mut kind) Miri.MIR.BorrowKind.Shared = isFalse ⋯
• Miri.MIR.instDecidableEqBorrowKind.decEq (Miri.MIR.BorrowKind.Mut kind) (Miri.MIR.BorrowKind.Fake kind_1) = isFalse ⋯
• Miri.MIR.instDecidableEqBorrowKind.decEq (Miri.MIR.BorrowKind.Mut a) (Miri.MIR.BorrowKind.Mut b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.RawPtrKind : Type

• Mut : RawPtrKind
• Const : RawPtrKind
• FakeForPtrMetadata : RawPtrKind

@[instance_reducible]

instance Miri.MIR.instReprRawPtrKind : Repr RawPtrKind

Equations

• Miri.MIR.instReprRawPtrKind = { reprPrec := Miri.MIR.instReprRawPtrKind.repr }

def Miri.MIR.instReprRawPtrKind.repr : RawPtrKind → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instReprRawPtrKind.repr Miri.MIR.RawPtrKind.Mut prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.RawPtrKind.Mut")).group prec✝
• Miri.MIR.instReprRawPtrKind.repr Miri.MIR.RawPtrKind.Const prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.RawPtrKind.Const")).group prec✝

@[instance_reducible]

instance Miri.MIR.instDecidableEqRawPtrKind : DecidableEq RawPtrKind

Equations

• Miri.MIR.instDecidableEqRawPtrKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.WithRetag : Type

• Yes : WithRetag
• No : WithRetag

def Miri.MIR.instReprWithRetag.repr : WithRetag → Nat → Std.Format

Equations

• Miri.MIR.instReprWithRetag.repr Miri.MIR.WithRetag.Yes prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.WithRetag.Yes")).group prec✝
• Miri.MIR.instReprWithRetag.repr Miri.MIR.WithRetag.No prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.WithRetag.No")).group prec✝

@[instance_reducible]

instance Miri.MIR.instReprWithRetag : Repr WithRetag

Equations

• Miri.MIR.instReprWithRetag = { reprPrec := Miri.MIR.instReprWithRetag.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqWithRetag : DecidableEq WithRetag

Equations

• Miri.MIR.instDecidableEqWithRetag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.RuntimeChecks : Type

• UbChecks : RuntimeChecks
• ContractChecks : RuntimeChecks
• OverflowChecks : RuntimeChecks

def Miri.MIR.instReprRuntimeChecks.repr : RuntimeChecks → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprRuntimeChecks : Repr RuntimeChecks

Equations

• Miri.MIR.instReprRuntimeChecks = { reprPrec := Miri.MIR.instReprRuntimeChecks.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqRuntimeChecks : DecidableEq RuntimeChecks

Equations

• Miri.MIR.instDecidableEqRuntimeChecks x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.LoopHintAttr : Type

• Hint : LoopHintAttr
• Full : LoopHintAttr
• Never : LoopHintAttr
• Count (count : Nat) : LoopHintAttr

@[instance_reducible]

instance Miri.MIR.instReprLoopHintAttr : Repr LoopHintAttr

Equations

• Miri.MIR.instReprLoopHintAttr = { reprPrec := Miri.MIR.instReprLoopHintAttr.repr }

def Miri.MIR.instReprLoopHintAttr.repr : LoopHintAttr → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqLoopHintAttr : DecidableEq LoopHintAttr

Equations

• Miri.MIR.instDecidableEqLoopHintAttr = Miri.MIR.instDecidableEqLoopHintAttr.decEq

def Miri.MIR.instDecidableEqLoopHintAttr.decEq (x✝ x✝¹ : LoopHintAttr) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqLoopHintAttr.decEq Miri.MIR.LoopHintAttr.Hint Miri.MIR.LoopHintAttr.Hint = isTrue ⋯
• Miri.MIR.instDecidableEqLoopHintAttr.decEq Miri.MIR.LoopHintAttr.Hint Miri.MIR.LoopHintAttr.Full = isFalse Miri.MIR.instDecidableEqLoopHintAttr.decEq._proof_1
• Miri.MIR.instDecidableEqLoopHintAttr.decEq Miri.MIR.LoopHintAttr.Hint Miri.MIR.LoopHintAttr.Never = isFalse Miri.MIR.instDecidableEqLoopHintAttr.decEq._proof_2
• Miri.MIR.instDecidableEqLoopHintAttr.decEq Miri.MIR.LoopHintAttr.Hint (Miri.MIR.LoopHintAttr.Count count) = isFalse ⋯
• Miri.MIR.instDecidableEqLoopHintAttr.decEq Miri.MIR.LoopHintAttr.Full Miri.MIR.LoopHintAttr.Hint = isFalse Miri.MIR.instDecidableEqLoopHintAttr.decEq._proof_4
• Miri.MIR.instDecidableEqLoopHintAttr.decEq Miri.MIR.LoopHintAttr.Full Miri.MIR.LoopHintAttr.Full = isTrue ⋯
• Miri.MIR.instDecidableEqLoopHintAttr.decEq Miri.MIR.LoopHintAttr.Full Miri.MIR.LoopHintAttr.Never = isFalse Miri.MIR.instDecidableEqLoopHintAttr.decEq._proof_5
• Miri.MIR.instDecidableEqLoopHintAttr.decEq Miri.MIR.LoopHintAttr.Full (Miri.MIR.LoopHintAttr.Count count) = isFalse ⋯
• Miri.MIR.instDecidableEqLoopHintAttr.decEq Miri.MIR.LoopHintAttr.Never Miri.MIR.LoopHintAttr.Hint = isFalse Miri.MIR.instDecidableEqLoopHintAttr.decEq._proof_7
• Miri.MIR.instDecidableEqLoopHintAttr.decEq Miri.MIR.LoopHintAttr.Never Miri.MIR.LoopHintAttr.Full = isFalse Miri.MIR.instDecidableEqLoopHintAttr.decEq._proof_8
• Miri.MIR.instDecidableEqLoopHintAttr.decEq Miri.MIR.LoopHintAttr.Never Miri.MIR.LoopHintAttr.Never = isTrue ⋯
• Miri.MIR.instDecidableEqLoopHintAttr.decEq Miri.MIR.LoopHintAttr.Never (Miri.MIR.LoopHintAttr.Count count) = isFalse ⋯
• Miri.MIR.instDecidableEqLoopHintAttr.decEq (Miri.MIR.LoopHintAttr.Count count) Miri.MIR.LoopHintAttr.Hint = isFalse ⋯
• Miri.MIR.instDecidableEqLoopHintAttr.decEq (Miri.MIR.LoopHintAttr.Count count) Miri.MIR.LoopHintAttr.Full = isFalse ⋯
• Miri.MIR.instDecidableEqLoopHintAttr.decEq (Miri.MIR.LoopHintAttr.Count count) Miri.MIR.LoopHintAttr.Never = isFalse ⋯
• Miri.MIR.instDecidableEqLoopHintAttr.decEq (Miri.MIR.LoopHintAttr.Count a) (Miri.MIR.LoopHintAttr.Count b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.FakeReadCause : Type

• ForMatchGuard : FakeReadCause
• ForMatchedPlace (closure : Option DefId) : FakeReadCause
• ForGuardBinding : FakeReadCause
• ForLet (closure : Option DefId) : FakeReadCause
• ForIndex : FakeReadCause

@[instance_reducible]

instance Miri.MIR.instReprFakeReadCause : Repr FakeReadCause

Equations

• Miri.MIR.instReprFakeReadCause = { reprPrec := Miri.MIR.instReprFakeReadCause.repr }

def Miri.MIR.instReprFakeReadCause.repr : FakeReadCause → Nat → Std.Format

Equations

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

def Miri.MIR.instDecidableEqFakeReadCause.decEq (x✝ x✝¹ : FakeReadCause) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForMatchGuard Miri.MIR.FakeReadCause.ForMatchGuard = isTrue ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForMatchGuard (Miri.MIR.FakeReadCause.ForMatchedPlace closure) = isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForMatchGuard Miri.MIR.FakeReadCause.ForGuardBinding = isFalse Miri.MIR.instDecidableEqFakeReadCause.decEq._proof_2
• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForMatchGuard (Miri.MIR.FakeReadCause.ForLet closure) = isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForMatchGuard Miri.MIR.FakeReadCause.ForIndex = isFalse Miri.MIR.instDecidableEqFakeReadCause.decEq._proof_4
• Miri.MIR.instDecidableEqFakeReadCause.decEq (Miri.MIR.FakeReadCause.ForMatchedPlace closure) Miri.MIR.FakeReadCause.ForMatchGuard = isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq (Miri.MIR.FakeReadCause.ForMatchedPlace a) (Miri.MIR.FakeReadCause.ForMatchedPlace b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq (Miri.MIR.FakeReadCause.ForMatchedPlace closure) Miri.MIR.FakeReadCause.ForGuardBinding = isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq (Miri.MIR.FakeReadCause.ForMatchedPlace closure) (Miri.MIR.FakeReadCause.ForLet closure_1) = isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq (Miri.MIR.FakeReadCause.ForMatchedPlace closure) Miri.MIR.FakeReadCause.ForIndex = isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForGuardBinding Miri.MIR.FakeReadCause.ForMatchGuard = isFalse Miri.MIR.instDecidableEqFakeReadCause.decEq._proof_11
• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForGuardBinding (Miri.MIR.FakeReadCause.ForMatchedPlace closure) = isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForGuardBinding Miri.MIR.FakeReadCause.ForGuardBinding = isTrue ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForGuardBinding (Miri.MIR.FakeReadCause.ForLet closure) = isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForGuardBinding Miri.MIR.FakeReadCause.ForIndex = isFalse Miri.MIR.instDecidableEqFakeReadCause.decEq._proof_14
• Miri.MIR.instDecidableEqFakeReadCause.decEq (Miri.MIR.FakeReadCause.ForLet closure) Miri.MIR.FakeReadCause.ForMatchGuard = isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq (Miri.MIR.FakeReadCause.ForLet closure) (Miri.MIR.FakeReadCause.ForMatchedPlace closure_1) = isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq (Miri.MIR.FakeReadCause.ForLet closure) Miri.MIR.FakeReadCause.ForGuardBinding = isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq (Miri.MIR.FakeReadCause.ForLet a) (Miri.MIR.FakeReadCause.ForLet b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq (Miri.MIR.FakeReadCause.ForLet closure) Miri.MIR.FakeReadCause.ForIndex = isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForIndex Miri.MIR.FakeReadCause.ForMatchGuard = isFalse Miri.MIR.instDecidableEqFakeReadCause.decEq._proof_21
• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForIndex (Miri.MIR.FakeReadCause.ForMatchedPlace closure) = isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForIndex Miri.MIR.FakeReadCause.ForGuardBinding = isFalse Miri.MIR.instDecidableEqFakeReadCause.decEq._proof_23
• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForIndex (Miri.MIR.FakeReadCause.ForLet closure) = isFalse ⋯
• Miri.MIR.instDecidableEqFakeReadCause.decEq Miri.MIR.FakeReadCause.ForIndex Miri.MIR.FakeReadCause.ForIndex = isTrue ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqFakeReadCause : DecidableEq FakeReadCause

Equations

• Miri.MIR.instDecidableEqFakeReadCause = Miri.MIR.instDecidableEqFakeReadCause.decEq

inductive Miri.MIR.CallSource : Type

• OverloadedOperator : CallSource
• MatchCmp : CallSource
• Misc : CallSource
• Use : CallSource
• Normal : CallSource

def Miri.MIR.instReprCallSource.repr : CallSource → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instReprCallSource.repr Miri.MIR.CallSource.Misc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.CallSource.Misc")).group prec✝
• Miri.MIR.instReprCallSource.repr Miri.MIR.CallSource.Use prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.CallSource.Use")).group prec✝
• Miri.MIR.instReprCallSource.repr Miri.MIR.CallSource.Normal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.CallSource.Normal")).group prec✝

@[instance_reducible]

instance Miri.MIR.instReprCallSource : Repr CallSource

Equations

• Miri.MIR.instReprCallSource = { reprPrec := Miri.MIR.instReprCallSource.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqCallSource : DecidableEq CallSource

Equations

• Miri.MIR.instDecidableEqCallSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.InlineAsmMacro : Type

• Asm : InlineAsmMacro
• NakedAsm : InlineAsmMacro

@[instance_reducible]

instance Miri.MIR.instReprInlineAsmMacro : Repr InlineAsmMacro

Equations

• Miri.MIR.instReprInlineAsmMacro = { reprPrec := Miri.MIR.instReprInlineAsmMacro.repr }

def Miri.MIR.instReprInlineAsmMacro.repr : InlineAsmMacro → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqInlineAsmMacro : DecidableEq InlineAsmMacro

Equations

• Miri.MIR.instDecidableEqInlineAsmMacro x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.UnwindTerminateReason : Type

• Abi : UnwindTerminateReason
• InCleanup : UnwindTerminateReason

def Miri.MIR.instReprUnwindTerminateReason.repr : UnwindTerminateReason → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprUnwindTerminateReason : Repr UnwindTerminateReason

Equations

• Miri.MIR.instReprUnwindTerminateReason = { reprPrec := Miri.MIR.instReprUnwindTerminateReason.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqUnwindTerminateReason : DecidableEq UnwindTerminateReason

Equations

• Miri.MIR.instDecidableEqUnwindTerminateReason x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.UnwindAction : Type

• Continue : UnwindAction
• Unreachable : UnwindAction
• Terminate (reason : UnwindTerminateReason) : UnwindAction
• Cleanup (target : BasicBlockId) : UnwindAction

@[instance_reducible]

instance Miri.MIR.instReprUnwindAction : Repr UnwindAction

Equations

• Miri.MIR.instReprUnwindAction = { reprPrec := Miri.MIR.instReprUnwindAction.repr }

def Miri.MIR.instReprUnwindAction.repr : UnwindAction → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqUnwindAction : DecidableEq UnwindAction

Equations

• Miri.MIR.instDecidableEqUnwindAction = Miri.MIR.instDecidableEqUnwindAction.decEq

def Miri.MIR.instDecidableEqUnwindAction.decEq (x✝ x✝¹ : UnwindAction) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqUnwindAction.decEq Miri.MIR.UnwindAction.Continue Miri.MIR.UnwindAction.Continue = isTrue ⋯
• Miri.MIR.instDecidableEqUnwindAction.decEq Miri.MIR.UnwindAction.Continue Miri.MIR.UnwindAction.Unreachable = isFalse Miri.MIR.instDecidableEqUnwindAction.decEq._proof_1
• Miri.MIR.instDecidableEqUnwindAction.decEq Miri.MIR.UnwindAction.Continue (Miri.MIR.UnwindAction.Terminate reason) = isFalse ⋯
• Miri.MIR.instDecidableEqUnwindAction.decEq Miri.MIR.UnwindAction.Continue (Miri.MIR.UnwindAction.Cleanup target) = isFalse ⋯
• Miri.MIR.instDecidableEqUnwindAction.decEq Miri.MIR.UnwindAction.Unreachable Miri.MIR.UnwindAction.Continue = isFalse Miri.MIR.instDecidableEqUnwindAction.decEq._proof_4
• Miri.MIR.instDecidableEqUnwindAction.decEq Miri.MIR.UnwindAction.Unreachable Miri.MIR.UnwindAction.Unreachable = isTrue ⋯
• Miri.MIR.instDecidableEqUnwindAction.decEq Miri.MIR.UnwindAction.Unreachable (Miri.MIR.UnwindAction.Terminate reason) = isFalse ⋯
• Miri.MIR.instDecidableEqUnwindAction.decEq Miri.MIR.UnwindAction.Unreachable (Miri.MIR.UnwindAction.Cleanup target) = isFalse ⋯
• Miri.MIR.instDecidableEqUnwindAction.decEq (Miri.MIR.UnwindAction.Terminate reason) Miri.MIR.UnwindAction.Continue = isFalse ⋯
• Miri.MIR.instDecidableEqUnwindAction.decEq (Miri.MIR.UnwindAction.Terminate reason) Miri.MIR.UnwindAction.Unreachable = isFalse ⋯
• Miri.MIR.instDecidableEqUnwindAction.decEq (Miri.MIR.UnwindAction.Terminate a) (Miri.MIR.UnwindAction.Terminate b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqUnwindAction.decEq (Miri.MIR.UnwindAction.Terminate reason) (Miri.MIR.UnwindAction.Cleanup target) = isFalse ⋯
• Miri.MIR.instDecidableEqUnwindAction.decEq (Miri.MIR.UnwindAction.Cleanup target) Miri.MIR.UnwindAction.Continue = isFalse ⋯
• Miri.MIR.instDecidableEqUnwindAction.decEq (Miri.MIR.UnwindAction.Cleanup target) Miri.MIR.UnwindAction.Unreachable = isFalse ⋯
• Miri.MIR.instDecidableEqUnwindAction.decEq (Miri.MIR.UnwindAction.Cleanup target) (Miri.MIR.UnwindAction.Terminate reason) = isFalse ⋯
• Miri.MIR.instDecidableEqUnwindAction.decEq (Miri.MIR.UnwindAction.Cleanup a) (Miri.MIR.UnwindAction.Cleanup b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.CoroutineSource : Type

• Block : CoroutineSource
• Closure : CoroutineSource
• Fn : CoroutineSource

def Miri.MIR.instReprCoroutineSource.repr : CoroutineSource → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprCoroutineSource : Repr CoroutineSource

Equations

• Miri.MIR.instReprCoroutineSource = { reprPrec := Miri.MIR.instReprCoroutineSource.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqCoroutineSource : DecidableEq CoroutineSource

Equations

• Miri.MIR.instDecidableEqCoroutineSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.CoroutineDesugaring : Type

• Async : CoroutineDesugaring
• Gen : CoroutineDesugaring
• AsyncGen : CoroutineDesugaring

def Miri.MIR.instReprCoroutineDesugaring.repr : CoroutineDesugaring → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprCoroutineDesugaring : Repr CoroutineDesugaring

Equations

• Miri.MIR.instReprCoroutineDesugaring = { reprPrec := Miri.MIR.instReprCoroutineDesugaring.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqCoroutineDesugaring : DecidableEq CoroutineDesugaring

Equations

• Miri.MIR.instDecidableEqCoroutineDesugaring x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.Movability : Type

• Static : Movability
• Movable : Movability

@[instance_reducible]

instance Miri.MIR.instReprMovability : Repr Movability

Equations

• Miri.MIR.instReprMovability = { reprPrec := Miri.MIR.instReprMovability.repr }

def Miri.MIR.instReprMovability.repr : Movability → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instReprMovability.repr Miri.MIR.Movability.Static prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.Movability.Static")).group prec✝

@[instance_reducible]

instance Miri.MIR.instDecidableEqMovability : DecidableEq Movability

Equations

• Miri.MIR.instDecidableEqMovability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.CoroutineKind : Type

• Desugared (kind : CoroutineDesugaring) (source : CoroutineSource) : CoroutineKind
• Coroutine (movability : Movability) : CoroutineKind

def Miri.MIR.instReprCoroutineKind.repr : CoroutineKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprCoroutineKind : Repr CoroutineKind

Equations

• Miri.MIR.instReprCoroutineKind = { reprPrec := Miri.MIR.instReprCoroutineKind.repr }

def Miri.MIR.instDecidableEqCoroutineKind.decEq (x✝ x✝¹ : CoroutineKind) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqCoroutineKind.decEq (Miri.MIR.CoroutineKind.Desugared kind source) (Miri.MIR.CoroutineKind.Coroutine movability) = isFalse ⋯
• Miri.MIR.instDecidableEqCoroutineKind.decEq (Miri.MIR.CoroutineKind.Coroutine movability) (Miri.MIR.CoroutineKind.Desugared kind source) = isFalse ⋯
• Miri.MIR.instDecidableEqCoroutineKind.decEq (Miri.MIR.CoroutineKind.Coroutine a) (Miri.MIR.CoroutineKind.Coroutine b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqCoroutineKind : DecidableEq CoroutineKind

Equations

• Miri.MIR.instDecidableEqCoroutineKind = Miri.MIR.instDecidableEqCoroutineKind.decEq

structure Miri.MIR.HirId : Type

• owner : HirOwnerId
• localId : HirLocalId

def Miri.MIR.instReprHirId.repr : HirId → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprHirId : Repr HirId

Equations

• Miri.MIR.instReprHirId = { reprPrec := Miri.MIR.instReprHirId.repr }

def Miri.MIR.instDecidableEqHirId.decEq (x✝ x✝¹ : HirId) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqHirId.decEq { owner := a, localId := a_1 } { owner := b, localId := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqHirId : DecidableEq HirId

Equations

• Miri.MIR.instDecidableEqHirId = Miri.MIR.instDecidableEqHirId.decEq

inductive Miri.MIR.CoveragePointKind : Type

• Expr : CoveragePointKind
• ImplicitElse : CoveragePointKind
• FunctionEnd : CoveragePointKind

@[instance_reducible]

instance Miri.MIR.instReprCoveragePointKind : Repr CoveragePointKind

Equations

• Miri.MIR.instReprCoveragePointKind = { reprPrec := Miri.MIR.instReprCoveragePointKind.repr }

def Miri.MIR.instReprCoveragePointKind.repr : CoveragePointKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqCoveragePointKind : DecidableEq CoveragePointKind

Equations

• Miri.MIR.instDecidableEqCoveragePointKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.CoverageKind : Type

• Point (pointKind : CoveragePointKind) (hirId : HirId) : CoverageKind
• BlockMarker (id : Nat) : CoverageKind
• VirtualCounter (basicCoverageBlock : Nat) : CoverageKind

def Miri.MIR.instReprCoverageKind.repr : CoverageKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprCoverageKind : Repr CoverageKind

Equations

• Miri.MIR.instReprCoverageKind = { reprPrec := Miri.MIR.instReprCoverageKind.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqCoverageKind : DecidableEq CoverageKind

Equations

• Miri.MIR.instDecidableEqCoverageKind = Miri.MIR.instDecidableEqCoverageKind.decEq

def Miri.MIR.instDecidableEqCoverageKind.decEq (x✝ x✝¹ : CoverageKind) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqCoverageKind.decEq (Miri.MIR.CoverageKind.Point pointKind hirId) (Miri.MIR.CoverageKind.BlockMarker id) = isFalse ⋯
• Miri.MIR.instDecidableEqCoverageKind.decEq (Miri.MIR.CoverageKind.Point pointKind hirId) (Miri.MIR.CoverageKind.VirtualCounter basicCoverageBlock) = isFalse ⋯
• Miri.MIR.instDecidableEqCoverageKind.decEq (Miri.MIR.CoverageKind.BlockMarker id) (Miri.MIR.CoverageKind.Point pointKind hirId) = isFalse ⋯
• Miri.MIR.instDecidableEqCoverageKind.decEq (Miri.MIR.CoverageKind.BlockMarker a) (Miri.MIR.CoverageKind.BlockMarker b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqCoverageKind.decEq (Miri.MIR.CoverageKind.BlockMarker id) (Miri.MIR.CoverageKind.VirtualCounter basicCoverageBlock) = isFalse ⋯
• Miri.MIR.instDecidableEqCoverageKind.decEq (Miri.MIR.CoverageKind.VirtualCounter basicCoverageBlock) (Miri.MIR.CoverageKind.Point pointKind hirId) = isFalse ⋯
• Miri.MIR.instDecidableEqCoverageKind.decEq (Miri.MIR.CoverageKind.VirtualCounter basicCoverageBlock) (Miri.MIR.CoverageKind.BlockMarker id) = isFalse ⋯
• Miri.MIR.instDecidableEqCoverageKind.decEq (Miri.MIR.CoverageKind.VirtualCounter a) (Miri.MIR.CoverageKind.VirtualCounter b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.BackwardIncompatibleDropReason : Type

• Edition2024 : BackwardIncompatibleDropReason

@[instance_reducible]

instance Miri.MIR.instReprBackwardIncompatibleDropReason : Repr BackwardIncompatibleDropReason

Equations

• Miri.MIR.instReprBackwardIncompatibleDropReason = { reprPrec := Miri.MIR.instReprBackwardIncompatibleDropReason.repr }

def Miri.MIR.instReprBackwardIncompatibleDropReason.repr : BackwardIncompatibleDropReason → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqBackwardIncompatibleDropReason : DecidableEq BackwardIncompatibleDropReason

Equations

• Miri.MIR.instDecidableEqBackwardIncompatibleDropReason x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.ProjectionKind : Type

• Deref : ProjectionKind
• Field (index : FieldIndex) : ProjectionKind
• Index : ProjectionKind
• ConstantIndex (offset minLength : Nat) (fromEnd : Bool) : ProjectionKind
• Subslice (fromIndex toIndex : Nat) (fromEnd : Bool) : ProjectionKind
• Downcast (name : Option String) (variant : VariantIndex) : ProjectionKind
• OpaqueCast : ProjectionKind
• UnwrapUnsafeBinder : ProjectionKind
• PhantomDeref : ProjectionKind

def Miri.MIR.instReprProjectionKind.repr : ProjectionKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprProjectionKind : Repr ProjectionKind

Equations

• Miri.MIR.instReprProjectionKind = { reprPrec := Miri.MIR.instReprProjectionKind.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqProjectionKind : DecidableEq ProjectionKind

Equations

• Miri.MIR.instDecidableEqProjectionKind = Miri.MIR.instDecidableEqProjectionKind.decEq

def Miri.MIR.instDecidableEqProjectionKind.decEq (x✝ x✝¹ : ProjectionKind) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Deref Miri.MIR.ProjectionKind.Deref = isTrue ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Deref (Miri.MIR.ProjectionKind.Field index) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Deref Miri.MIR.ProjectionKind.Index = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_2
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Deref (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Deref (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Deref (Miri.MIR.ProjectionKind.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Deref Miri.MIR.ProjectionKind.OpaqueCast = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_6
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Deref Miri.MIR.ProjectionKind.UnwrapUnsafeBinder = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_7
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Deref Miri.MIR.ProjectionKind.PhantomDeref = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_8
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Field index) Miri.MIR.ProjectionKind.Deref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Field a) (Miri.MIR.ProjectionKind.Field b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Field index) Miri.MIR.ProjectionKind.Index = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Field index) (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Field index) (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Field index) (Miri.MIR.ProjectionKind.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Field index) Miri.MIR.ProjectionKind.OpaqueCast = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Field index) Miri.MIR.ProjectionKind.UnwrapUnsafeBinder = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Field index) Miri.MIR.ProjectionKind.PhantomDeref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Index Miri.MIR.ProjectionKind.Deref = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_19
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Index (Miri.MIR.ProjectionKind.Field index) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Index Miri.MIR.ProjectionKind.Index = isTrue ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Index (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Index (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Index (Miri.MIR.ProjectionKind.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Index Miri.MIR.ProjectionKind.OpaqueCast = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_24
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Index Miri.MIR.ProjectionKind.UnwrapUnsafeBinder = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_25
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.Index Miri.MIR.ProjectionKind.PhantomDeref = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_26
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) Miri.MIR.ProjectionKind.Deref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) (Miri.MIR.ProjectionKind.Field index) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) Miri.MIR.ProjectionKind.Index = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd_1) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) (Miri.MIR.ProjectionKind.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) Miri.MIR.ProjectionKind.OpaqueCast = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) Miri.MIR.ProjectionKind.UnwrapUnsafeBinder = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) Miri.MIR.ProjectionKind.PhantomDeref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) Miri.MIR.ProjectionKind.Deref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) (Miri.MIR.ProjectionKind.Field index) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) Miri.MIR.ProjectionKind.Index = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd_1) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) (Miri.MIR.ProjectionKind.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) Miri.MIR.ProjectionKind.OpaqueCast = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) Miri.MIR.ProjectionKind.UnwrapUnsafeBinder = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) Miri.MIR.ProjectionKind.PhantomDeref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Downcast name variant) Miri.MIR.ProjectionKind.Deref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Downcast name variant) (Miri.MIR.ProjectionKind.Field index) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Downcast name variant) Miri.MIR.ProjectionKind.Index = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Downcast name variant) (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Downcast name variant) (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Downcast name variant) Miri.MIR.ProjectionKind.OpaqueCast = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Downcast name variant) Miri.MIR.ProjectionKind.UnwrapUnsafeBinder = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq (Miri.MIR.ProjectionKind.Downcast name variant) Miri.MIR.ProjectionKind.PhantomDeref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.OpaqueCast Miri.MIR.ProjectionKind.Deref = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_62
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.OpaqueCast (Miri.MIR.ProjectionKind.Field index) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.OpaqueCast Miri.MIR.ProjectionKind.Index = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_64
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.OpaqueCast (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.OpaqueCast (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.OpaqueCast (Miri.MIR.ProjectionKind.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.OpaqueCast Miri.MIR.ProjectionKind.OpaqueCast = isTrue ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.OpaqueCast Miri.MIR.ProjectionKind.UnwrapUnsafeBinder = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_68
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.OpaqueCast Miri.MIR.ProjectionKind.PhantomDeref = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_69
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.UnwrapUnsafeBinder Miri.MIR.ProjectionKind.Deref = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_70
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.UnwrapUnsafeBinder (Miri.MIR.ProjectionKind.Field index) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.UnwrapUnsafeBinder Miri.MIR.ProjectionKind.Index = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_72
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.UnwrapUnsafeBinder (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.UnwrapUnsafeBinder (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.UnwrapUnsafeBinder (Miri.MIR.ProjectionKind.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.UnwrapUnsafeBinder Miri.MIR.ProjectionKind.OpaqueCast = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_76
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.UnwrapUnsafeBinder Miri.MIR.ProjectionKind.UnwrapUnsafeBinder = isTrue ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.UnwrapUnsafeBinder Miri.MIR.ProjectionKind.PhantomDeref = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_77
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.PhantomDeref Miri.MIR.ProjectionKind.Deref = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_78
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.PhantomDeref (Miri.MIR.ProjectionKind.Field index) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.PhantomDeref Miri.MIR.ProjectionKind.Index = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_80
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.PhantomDeref (Miri.MIR.ProjectionKind.ConstantIndex offset minLength fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.PhantomDeref (Miri.MIR.ProjectionKind.Subslice fromIndex toIndex fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.PhantomDeref (Miri.MIR.ProjectionKind.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.PhantomDeref Miri.MIR.ProjectionKind.OpaqueCast = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_84
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.PhantomDeref Miri.MIR.ProjectionKind.UnwrapUnsafeBinder = isFalse Miri.MIR.instDecidableEqProjectionKind.decEq._proof_85
• Miri.MIR.instDecidableEqProjectionKind.decEq Miri.MIR.ProjectionKind.PhantomDeref Miri.MIR.ProjectionKind.PhantomDeref = isTrue ⋯

structure Miri.MIR.UserTypeProjection : Type

• base : UserTypeAnnotationIndex
• projections : Array ProjectionKind

def Miri.MIR.instReprUserTypeProjection.repr : UserTypeProjection → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprUserTypeProjection : Repr UserTypeProjection

Equations

• Miri.MIR.instReprUserTypeProjection = { reprPrec := Miri.MIR.instReprUserTypeProjection.repr }

def Miri.MIR.instDecidableEqUserTypeProjection.decEq (x✝ x✝¹ : UserTypeProjection) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqUserTypeProjection : DecidableEq UserTypeProjection

Equations

• Miri.MIR.instDecidableEqUserTypeProjection = Miri.MIR.instDecidableEqUserTypeProjection.decEq

inductive Miri.MIR.AnalysisPhase : Type

• Initial : AnalysisPhase
• PostCleanup : AnalysisPhase

@[instance_reducible]

instance Miri.MIR.instReprAnalysisPhase : Repr AnalysisPhase

Equations

• Miri.MIR.instReprAnalysisPhase = { reprPrec := Miri.MIR.instReprAnalysisPhase.repr }

def Miri.MIR.instReprAnalysisPhase.repr : AnalysisPhase → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqAnalysisPhase : DecidableEq AnalysisPhase

Equations

• Miri.MIR.instDecidableEqAnalysisPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.RuntimePhase : Type

• Initial : RuntimePhase
• PostCleanup : RuntimePhase
• Optimized : RuntimePhase

def Miri.MIR.instReprRuntimePhase.repr : RuntimePhase → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprRuntimePhase : Repr RuntimePhase

Equations

• Miri.MIR.instReprRuntimePhase = { reprPrec := Miri.MIR.instReprRuntimePhase.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqRuntimePhase : DecidableEq RuntimePhase

Equations

• Miri.MIR.instDecidableEqRuntimePhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.MirPhase : Type

• Built : MirPhase
• Analysis (phase : AnalysisPhase) : MirPhase
• Runtime (phase : RuntimePhase) : MirPhase

@[instance_reducible]

instance Miri.MIR.instReprMirPhase : Repr MirPhase

Equations

• Miri.MIR.instReprMirPhase = { reprPrec := Miri.MIR.instReprMirPhase.repr }

def Miri.MIR.instReprMirPhase.repr : MirPhase → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instReprMirPhase.repr Miri.MIR.MirPhase.Built prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.MirPhase.Built")).group prec✝

def Miri.MIR.instDecidableEqMirPhase.decEq (x✝ x✝¹ : MirPhase) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqMirPhase.decEq Miri.MIR.MirPhase.Built Miri.MIR.MirPhase.Built = isTrue ⋯
• Miri.MIR.instDecidableEqMirPhase.decEq Miri.MIR.MirPhase.Built (Miri.MIR.MirPhase.Analysis phase) = isFalse ⋯
• Miri.MIR.instDecidableEqMirPhase.decEq Miri.MIR.MirPhase.Built (Miri.MIR.MirPhase.Runtime phase) = isFalse ⋯
• Miri.MIR.instDecidableEqMirPhase.decEq (Miri.MIR.MirPhase.Analysis phase) Miri.MIR.MirPhase.Built = isFalse ⋯
• Miri.MIR.instDecidableEqMirPhase.decEq (Miri.MIR.MirPhase.Analysis a) (Miri.MIR.MirPhase.Analysis b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqMirPhase.decEq (Miri.MIR.MirPhase.Analysis phase) (Miri.MIR.MirPhase.Runtime phase_1) = isFalse ⋯
• Miri.MIR.instDecidableEqMirPhase.decEq (Miri.MIR.MirPhase.Runtime phase) Miri.MIR.MirPhase.Built = isFalse ⋯
• Miri.MIR.instDecidableEqMirPhase.decEq (Miri.MIR.MirPhase.Runtime phase) (Miri.MIR.MirPhase.Analysis phase_1) = isFalse ⋯
• Miri.MIR.instDecidableEqMirPhase.decEq (Miri.MIR.MirPhase.Runtime a) (Miri.MIR.MirPhase.Runtime b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqMirPhase : DecidableEq MirPhase

Equations

• Miri.MIR.instDecidableEqMirPhase = Miri.MIR.instDecidableEqMirPhase.decEq

Constant values and type-system constants are explicit trees. ScalarBits stores the exact low-bit encoding together with its byte width. Pointer scalar provenance remains an allocation-graph identity and is not a runtime AllocId.

inductive Miri.MIR.ConstPointer : Type

• Allocation (allocation : AllocationId) (offsetBytes : Nat) (immutable sharedRef : Bool) : ConstPointer
• Address (address widthBytes : Nat) : ConstPointer

def Miri.MIR.instReprConstPointer.repr : ConstPointer → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprConstPointer : Repr ConstPointer

Equations

• Miri.MIR.instReprConstPointer = { reprPrec := Miri.MIR.instReprConstPointer.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqConstPointer : DecidableEq ConstPointer

Equations

• Miri.MIR.instDecidableEqConstPointer = Miri.MIR.instDecidableEqConstPointer.decEq

def Miri.MIR.instDecidableEqConstPointer.decEq (x✝ x✝¹ : ConstPointer) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqConstPointer.decEq (Miri.MIR.ConstPointer.Allocation allocation offsetBytes immutable sharedRef) (Miri.MIR.ConstPointer.Address address widthBytes) = isFalse ⋯
• Miri.MIR.instDecidableEqConstPointer.decEq (Miri.MIR.ConstPointer.Address address widthBytes) (Miri.MIR.ConstPointer.Allocation allocation offsetBytes immutable sharedRef) = isFalse ⋯

inductive Miri.MIR.ScalarValue : Type

• Int (bits sizeBytes : Nat) : ScalarValue
• Ptr (pointer : ConstPointer) : ScalarValue

def Miri.MIR.instReprScalarValue.repr : ScalarValue → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprScalarValue : Repr ScalarValue

Equations

• Miri.MIR.instReprScalarValue = { reprPrec := Miri.MIR.instReprScalarValue.repr }

def Miri.MIR.instDecidableEqScalarValue.decEq (x✝ x✝¹ : ScalarValue) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqScalarValue.decEq (Miri.MIR.ScalarValue.Int a a_1) (Miri.MIR.ScalarValue.Int b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqScalarValue.decEq (Miri.MIR.ScalarValue.Int bits sizeBytes) (Miri.MIR.ScalarValue.Ptr pointer) = isFalse ⋯
• Miri.MIR.instDecidableEqScalarValue.decEq (Miri.MIR.ScalarValue.Ptr pointer) (Miri.MIR.ScalarValue.Int bits sizeBytes) = isFalse ⋯
• Miri.MIR.instDecidableEqScalarValue.decEq (Miri.MIR.ScalarValue.Ptr a) (Miri.MIR.ScalarValue.Ptr b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqScalarValue : DecidableEq ScalarValue

Equations

• Miri.MIR.instDecidableEqScalarValue = Miri.MIR.instDecidableEqScalarValue.decEq

inductive Miri.MIR.ConstValue : Type

• Scalar (value : ScalarValue) : ConstValue
• ZeroSized : ConstValue
• Slice (allocation : AllocationId) (metadata : Nat) : ConstValue
• Indirect (allocation : AllocationId) (offsetBytes : Nat) : ConstValue

@[instance_reducible]

instance Miri.MIR.instReprConstValue : Repr ConstValue

Equations

• Miri.MIR.instReprConstValue = { reprPrec := Miri.MIR.instReprConstValue.repr }

def Miri.MIR.instReprConstValue.repr : ConstValue → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqConstValue : DecidableEq ConstValue

Equations

• Miri.MIR.instDecidableEqConstValue = Miri.MIR.instDecidableEqConstValue.decEq

def Miri.MIR.instDecidableEqConstValue.decEq (x✝ x✝¹ : ConstValue) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqConstValue.decEq (Miri.MIR.ConstValue.Scalar a) (Miri.MIR.ConstValue.Scalar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqConstValue.decEq (Miri.MIR.ConstValue.Scalar value) Miri.MIR.ConstValue.ZeroSized = isFalse ⋯
• Miri.MIR.instDecidableEqConstValue.decEq (Miri.MIR.ConstValue.Scalar value) (Miri.MIR.ConstValue.Slice allocation metadata) = isFalse ⋯
• Miri.MIR.instDecidableEqConstValue.decEq (Miri.MIR.ConstValue.Scalar value) (Miri.MIR.ConstValue.Indirect allocation offsetBytes) = isFalse ⋯
• Miri.MIR.instDecidableEqConstValue.decEq Miri.MIR.ConstValue.ZeroSized (Miri.MIR.ConstValue.Scalar value) = isFalse ⋯
• Miri.MIR.instDecidableEqConstValue.decEq Miri.MIR.ConstValue.ZeroSized Miri.MIR.ConstValue.ZeroSized = isTrue ⋯
• Miri.MIR.instDecidableEqConstValue.decEq Miri.MIR.ConstValue.ZeroSized (Miri.MIR.ConstValue.Slice allocation metadata) = isFalse ⋯
• Miri.MIR.instDecidableEqConstValue.decEq Miri.MIR.ConstValue.ZeroSized (Miri.MIR.ConstValue.Indirect allocation offsetBytes) = isFalse ⋯
• Miri.MIR.instDecidableEqConstValue.decEq (Miri.MIR.ConstValue.Slice allocation metadata) (Miri.MIR.ConstValue.Scalar value) = isFalse ⋯
• Miri.MIR.instDecidableEqConstValue.decEq (Miri.MIR.ConstValue.Slice allocation metadata) Miri.MIR.ConstValue.ZeroSized = isFalse ⋯
• Miri.MIR.instDecidableEqConstValue.decEq (Miri.MIR.ConstValue.Slice a a_1) (Miri.MIR.ConstValue.Slice b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqConstValue.decEq (Miri.MIR.ConstValue.Slice allocation metadata) (Miri.MIR.ConstValue.Indirect allocation_1 offsetBytes) = isFalse ⋯
• Miri.MIR.instDecidableEqConstValue.decEq (Miri.MIR.ConstValue.Indirect allocation offsetBytes) (Miri.MIR.ConstValue.Scalar value) = isFalse ⋯
• Miri.MIR.instDecidableEqConstValue.decEq (Miri.MIR.ConstValue.Indirect allocation offsetBytes) Miri.MIR.ConstValue.ZeroSized = isFalse ⋯
• Miri.MIR.instDecidableEqConstValue.decEq (Miri.MIR.ConstValue.Indirect allocation offsetBytes) (Miri.MIR.ConstValue.Slice allocation_1 metadata) = isFalse ⋯

inductive Miri.MIR.ConstAliasKind : Type

• Projection : ConstAliasKind
• InherentSelf : ConstAliasKind
• InherentImpl : ConstAliasKind
• Free : ConstAliasKind
• Anon : ConstAliasKind

def Miri.MIR.instReprConstAliasKind.repr : ConstAliasKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprConstAliasKind : Repr ConstAliasKind

Equations

• Miri.MIR.instReprConstAliasKind = { reprPrec := Miri.MIR.instReprConstAliasKind.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqConstAliasKind : DecidableEq ConstAliasKind

Equations

• Miri.MIR.instDecidableEqConstAliasKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.ConstExpressionCastKind : Type

• As : ConstExpressionCastKind
• Use : ConstExpressionCastKind

def Miri.MIR.instReprConstExpressionCastKind.repr : ConstExpressionCastKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprConstExpressionCastKind : Repr ConstExpressionCastKind

Equations

• Miri.MIR.instReprConstExpressionCastKind = { reprPrec := Miri.MIR.instReprConstExpressionCastKind.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqConstExpressionCastKind : DecidableEq ConstExpressionCastKind

Equations

• Miri.MIR.instDecidableEqConstExpressionCastKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.ConstExpressionKind : Type

• Binop (operator : BinOp) : ConstExpressionKind
• UnOp (operator : MIR.UnOp) : ConstExpressionKind
• FunctionCall : ConstExpressionKind
• Cast (kind : ConstExpressionCastKind) : ConstExpressionKind

@[instance_reducible]

instance Miri.MIR.instReprConstExpressionKind : Repr ConstExpressionKind

Equations

• Miri.MIR.instReprConstExpressionKind = { reprPrec := Miri.MIR.instReprConstExpressionKind.repr }

def Miri.MIR.instReprConstExpressionKind.repr : ConstExpressionKind → Nat → Std.Format

Equations

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

def Miri.MIR.instDecidableEqConstExpressionKind.decEq (x✝ x✝¹ : ConstExpressionKind) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqConstExpressionKind.decEq (Miri.MIR.ConstExpressionKind.Binop a) (Miri.MIR.ConstExpressionKind.Binop b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq (Miri.MIR.ConstExpressionKind.Binop operator) (Miri.MIR.ConstExpressionKind.UnOp operator_1) = isFalse ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq (Miri.MIR.ConstExpressionKind.Binop operator) Miri.MIR.ConstExpressionKind.FunctionCall = isFalse ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq (Miri.MIR.ConstExpressionKind.Binop operator) (Miri.MIR.ConstExpressionKind.Cast kind) = isFalse ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq (Miri.MIR.ConstExpressionKind.UnOp operator) (Miri.MIR.ConstExpressionKind.Binop operator_1) = isFalse ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq (Miri.MIR.ConstExpressionKind.UnOp a) (Miri.MIR.ConstExpressionKind.UnOp b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq (Miri.MIR.ConstExpressionKind.UnOp operator) Miri.MIR.ConstExpressionKind.FunctionCall = isFalse ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq (Miri.MIR.ConstExpressionKind.UnOp operator) (Miri.MIR.ConstExpressionKind.Cast kind) = isFalse ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq Miri.MIR.ConstExpressionKind.FunctionCall (Miri.MIR.ConstExpressionKind.Binop operator) = isFalse ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq Miri.MIR.ConstExpressionKind.FunctionCall (Miri.MIR.ConstExpressionKind.UnOp operator) = isFalse ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq Miri.MIR.ConstExpressionKind.FunctionCall Miri.MIR.ConstExpressionKind.FunctionCall = isTrue ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq Miri.MIR.ConstExpressionKind.FunctionCall (Miri.MIR.ConstExpressionKind.Cast kind) = isFalse ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq (Miri.MIR.ConstExpressionKind.Cast kind) (Miri.MIR.ConstExpressionKind.Binop operator) = isFalse ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq (Miri.MIR.ConstExpressionKind.Cast kind) (Miri.MIR.ConstExpressionKind.UnOp operator) = isFalse ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq (Miri.MIR.ConstExpressionKind.Cast kind) Miri.MIR.ConstExpressionKind.FunctionCall = isFalse ⋯
• Miri.MIR.instDecidableEqConstExpressionKind.decEq (Miri.MIR.ConstExpressionKind.Cast a) (Miri.MIR.ConstExpressionKind.Cast b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqConstExpressionKind : DecidableEq ConstExpressionKind

Equations

• Miri.MIR.instDecidableEqConstExpressionKind = Miri.MIR.instDecidableEqConstExpressionKind.decEq

inductive Miri.MIR.BoundVarIndexKind : Type

• Bound (debruijnIndex : Nat) : BoundVarIndexKind
• Canonical : BoundVarIndexKind

def Miri.MIR.instReprBoundVarIndexKind.repr : BoundVarIndexKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprBoundVarIndexKind : Repr BoundVarIndexKind

Equations

• Miri.MIR.instReprBoundVarIndexKind = { reprPrec := Miri.MIR.instReprBoundVarIndexKind.repr }

def Miri.MIR.instDecidableEqBoundVarIndexKind.decEq (x✝ x✝¹ : BoundVarIndexKind) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqBoundVarIndexKind.decEq (Miri.MIR.BoundVarIndexKind.Bound a) (Miri.MIR.BoundVarIndexKind.Bound b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqBoundVarIndexKind.decEq (Miri.MIR.BoundVarIndexKind.Bound debruijnIndex) Miri.MIR.BoundVarIndexKind.Canonical = isFalse ⋯
• Miri.MIR.instDecidableEqBoundVarIndexKind.decEq Miri.MIR.BoundVarIndexKind.Canonical (Miri.MIR.BoundVarIndexKind.Bound debruijnIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqBoundVarIndexKind.decEq Miri.MIR.BoundVarIndexKind.Canonical Miri.MIR.BoundVarIndexKind.Canonical = isTrue ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqBoundVarIndexKind : DecidableEq BoundVarIndexKind

Equations

• Miri.MIR.instDecidableEqBoundVarIndexKind = Miri.MIR.instDecidableEqBoundVarIndexKind.decEq

inductive Miri.MIR.BoundRegionKind : Type

• Anon : BoundRegionKind
• NamedForPrinting (name : String) : BoundRegionKind
• Named (definition : DefId) : BoundRegionKind
• ClosureEnv : BoundRegionKind

def Miri.MIR.instReprBoundRegionKind.repr : BoundRegionKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprBoundRegionKind : Repr BoundRegionKind

Equations

• Miri.MIR.instReprBoundRegionKind = { reprPrec := Miri.MIR.instReprBoundRegionKind.repr }

def Miri.MIR.instDecidableEqBoundRegionKind.decEq (x✝ x✝¹ : BoundRegionKind) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqBoundRegionKind.decEq Miri.MIR.BoundRegionKind.Anon Miri.MIR.BoundRegionKind.Anon = isTrue ⋯
• Miri.MIR.instDecidableEqBoundRegionKind.decEq Miri.MIR.BoundRegionKind.Anon (Miri.MIR.BoundRegionKind.NamedForPrinting name) = isFalse ⋯
• Miri.MIR.instDecidableEqBoundRegionKind.decEq Miri.MIR.BoundRegionKind.Anon (Miri.MIR.BoundRegionKind.Named definition) = isFalse ⋯
• Miri.MIR.instDecidableEqBoundRegionKind.decEq Miri.MIR.BoundRegionKind.Anon Miri.MIR.BoundRegionKind.ClosureEnv = isFalse Miri.MIR.instDecidableEqBoundRegionKind.decEq._proof_3
• Miri.MIR.instDecidableEqBoundRegionKind.decEq (Miri.MIR.BoundRegionKind.NamedForPrinting name) Miri.MIR.BoundRegionKind.Anon = isFalse ⋯
• Miri.MIR.instDecidableEqBoundRegionKind.decEq (Miri.MIR.BoundRegionKind.NamedForPrinting a) (Miri.MIR.BoundRegionKind.NamedForPrinting b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqBoundRegionKind.decEq (Miri.MIR.BoundRegionKind.NamedForPrinting name) (Miri.MIR.BoundRegionKind.Named definition) = isFalse ⋯
• Miri.MIR.instDecidableEqBoundRegionKind.decEq (Miri.MIR.BoundRegionKind.NamedForPrinting name) Miri.MIR.BoundRegionKind.ClosureEnv = isFalse ⋯
• Miri.MIR.instDecidableEqBoundRegionKind.decEq (Miri.MIR.BoundRegionKind.Named definition) Miri.MIR.BoundRegionKind.Anon = isFalse ⋯
• Miri.MIR.instDecidableEqBoundRegionKind.decEq (Miri.MIR.BoundRegionKind.Named definition) (Miri.MIR.BoundRegionKind.NamedForPrinting name) = isFalse ⋯
• Miri.MIR.instDecidableEqBoundRegionKind.decEq (Miri.MIR.BoundRegionKind.Named a) (Miri.MIR.BoundRegionKind.Named b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqBoundRegionKind.decEq (Miri.MIR.BoundRegionKind.Named definition) Miri.MIR.BoundRegionKind.ClosureEnv = isFalse ⋯
• Miri.MIR.instDecidableEqBoundRegionKind.decEq Miri.MIR.BoundRegionKind.ClosureEnv Miri.MIR.BoundRegionKind.Anon = isFalse Miri.MIR.instDecidableEqBoundRegionKind.decEq._proof_14
• Miri.MIR.instDecidableEqBoundRegionKind.decEq Miri.MIR.BoundRegionKind.ClosureEnv (Miri.MIR.BoundRegionKind.NamedForPrinting name) = isFalse ⋯
• Miri.MIR.instDecidableEqBoundRegionKind.decEq Miri.MIR.BoundRegionKind.ClosureEnv (Miri.MIR.BoundRegionKind.Named definition) = isFalse ⋯
• Miri.MIR.instDecidableEqBoundRegionKind.decEq Miri.MIR.BoundRegionKind.ClosureEnv Miri.MIR.BoundRegionKind.ClosureEnv = isTrue ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqBoundRegionKind : DecidableEq BoundRegionKind

Equations

• Miri.MIR.instDecidableEqBoundRegionKind = Miri.MIR.instDecidableEqBoundRegionKind.decEq

inductive Miri.MIR.BoundTypeKind : Type

• Anon : BoundTypeKind
• Param (definition : DefId) : BoundTypeKind

@[instance_reducible]

instance Miri.MIR.instReprBoundTypeKind : Repr BoundTypeKind

Equations

• Miri.MIR.instReprBoundTypeKind = { reprPrec := Miri.MIR.instReprBoundTypeKind.repr }

def Miri.MIR.instReprBoundTypeKind.repr : BoundTypeKind → Nat → Std.Format

Equations

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

def Miri.MIR.instDecidableEqBoundTypeKind.decEq (x✝ x✝¹ : BoundTypeKind) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqBoundTypeKind.decEq Miri.MIR.BoundTypeKind.Anon Miri.MIR.BoundTypeKind.Anon = isTrue ⋯
• Miri.MIR.instDecidableEqBoundTypeKind.decEq Miri.MIR.BoundTypeKind.Anon (Miri.MIR.BoundTypeKind.Param definition) = isFalse ⋯
• Miri.MIR.instDecidableEqBoundTypeKind.decEq (Miri.MIR.BoundTypeKind.Param definition) Miri.MIR.BoundTypeKind.Anon = isFalse ⋯
• Miri.MIR.instDecidableEqBoundTypeKind.decEq (Miri.MIR.BoundTypeKind.Param a) (Miri.MIR.BoundTypeKind.Param b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqBoundTypeKind : DecidableEq BoundTypeKind

Equations

• Miri.MIR.instDecidableEqBoundTypeKind = Miri.MIR.instDecidableEqBoundTypeKind.decEq

inductive Miri.MIR.BoundVariableKind : Type

• Type (kind : BoundTypeKind) : BoundVariableKind
• Region (kind : BoundRegionKind) : BoundVariableKind
• Const : BoundVariableKind

@[instance_reducible]

instance Miri.MIR.instReprBoundVariableKind : Repr BoundVariableKind

Equations

• Miri.MIR.instReprBoundVariableKind = { reprPrec := Miri.MIR.instReprBoundVariableKind.repr }

def Miri.MIR.instReprBoundVariableKind.repr : BoundVariableKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqBoundVariableKind : DecidableEq BoundVariableKind

Equations

• Miri.MIR.instDecidableEqBoundVariableKind = Miri.MIR.instDecidableEqBoundVariableKind.decEq

def Miri.MIR.instDecidableEqBoundVariableKind.decEq (x✝ x✝¹ : BoundVariableKind) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqBoundVariableKind.decEq (Miri.MIR.BoundVariableKind.Type a) (Miri.MIR.BoundVariableKind.Type b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqBoundVariableKind.decEq (Miri.MIR.BoundVariableKind.Type kind) (Miri.MIR.BoundVariableKind.Region kind_1) = isFalse ⋯
• Miri.MIR.instDecidableEqBoundVariableKind.decEq (Miri.MIR.BoundVariableKind.Type kind) Miri.MIR.BoundVariableKind.Const = isFalse ⋯
• Miri.MIR.instDecidableEqBoundVariableKind.decEq (Miri.MIR.BoundVariableKind.Region kind) (Miri.MIR.BoundVariableKind.Type kind_1) = isFalse ⋯
• Miri.MIR.instDecidableEqBoundVariableKind.decEq (Miri.MIR.BoundVariableKind.Region a) (Miri.MIR.BoundVariableKind.Region b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqBoundVariableKind.decEq (Miri.MIR.BoundVariableKind.Region kind) Miri.MIR.BoundVariableKind.Const = isFalse ⋯
• Miri.MIR.instDecidableEqBoundVariableKind.decEq Miri.MIR.BoundVariableKind.Const (Miri.MIR.BoundVariableKind.Type kind) = isFalse ⋯
• Miri.MIR.instDecidableEqBoundVariableKind.decEq Miri.MIR.BoundVariableKind.Const (Miri.MIR.BoundVariableKind.Region kind) = isFalse ⋯
• Miri.MIR.instDecidableEqBoundVariableKind.decEq Miri.MIR.BoundVariableKind.Const Miri.MIR.BoundVariableKind.Const = isTrue ⋯

inductive Miri.MIR.LateParamRegionKind : Type

• Anon (index : Nat) : LateParamRegionKind
• NamedAnon (index : Nat) (name : String) : LateParamRegionKind
• Named (definition : DefId) : LateParamRegionKind
• ClosureEnv : LateParamRegionKind

@[instance_reducible]

instance Miri.MIR.instReprLateParamRegionKind : Repr LateParamRegionKind

Equations

• Miri.MIR.instReprLateParamRegionKind = { reprPrec := Miri.MIR.instReprLateParamRegionKind.repr }

def Miri.MIR.instReprLateParamRegionKind.repr : LateParamRegionKind → Nat → Std.Format

Equations

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

def Miri.MIR.instDecidableEqLateParamRegionKind.decEq (x✝ x✝¹ : LateParamRegionKind) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq (Miri.MIR.LateParamRegionKind.Anon a) (Miri.MIR.LateParamRegionKind.Anon b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq (Miri.MIR.LateParamRegionKind.Anon index) (Miri.MIR.LateParamRegionKind.NamedAnon index_1 name) = isFalse ⋯
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq (Miri.MIR.LateParamRegionKind.Anon index) (Miri.MIR.LateParamRegionKind.Named definition) = isFalse ⋯
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq (Miri.MIR.LateParamRegionKind.Anon index) Miri.MIR.LateParamRegionKind.ClosureEnv = isFalse ⋯
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq (Miri.MIR.LateParamRegionKind.NamedAnon index name) (Miri.MIR.LateParamRegionKind.Anon index_1) = isFalse ⋯
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq (Miri.MIR.LateParamRegionKind.NamedAnon index name) (Miri.MIR.LateParamRegionKind.Named definition) = isFalse ⋯
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq (Miri.MIR.LateParamRegionKind.NamedAnon index name) Miri.MIR.LateParamRegionKind.ClosureEnv = isFalse ⋯
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq (Miri.MIR.LateParamRegionKind.Named definition) (Miri.MIR.LateParamRegionKind.Anon index) = isFalse ⋯
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq (Miri.MIR.LateParamRegionKind.Named definition) (Miri.MIR.LateParamRegionKind.NamedAnon index name) = isFalse ⋯
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq (Miri.MIR.LateParamRegionKind.Named a) (Miri.MIR.LateParamRegionKind.Named b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq (Miri.MIR.LateParamRegionKind.Named definition) Miri.MIR.LateParamRegionKind.ClosureEnv = isFalse ⋯
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq Miri.MIR.LateParamRegionKind.ClosureEnv (Miri.MIR.LateParamRegionKind.Anon index) = isFalse ⋯
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq Miri.MIR.LateParamRegionKind.ClosureEnv (Miri.MIR.LateParamRegionKind.NamedAnon index name) = isFalse ⋯
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq Miri.MIR.LateParamRegionKind.ClosureEnv (Miri.MIR.LateParamRegionKind.Named definition) = isFalse ⋯
• Miri.MIR.instDecidableEqLateParamRegionKind.decEq Miri.MIR.LateParamRegionKind.ClosureEnv Miri.MIR.LateParamRegionKind.ClosureEnv = isTrue ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqLateParamRegionKind : DecidableEq LateParamRegionKind

Equations

• Miri.MIR.instDecidableEqLateParamRegionKind = Miri.MIR.instDecidableEqLateParamRegionKind.decEq

inductive Miri.MIR.Region : Type

• EarlyParameter (index : Nat) (name : String) : Region
• Bound (indexKind : BoundVarIndexKind) (variableIndex : Nat) (kind : BoundRegionKind) : Region
• LateParameter (scope : DefId) (kind : LateParamRegionKind) : Region
• Static : Region
• InferenceVariable (index : Nat) : Region
• Placeholder (universeIndex variableIndex : Nat) (kind : BoundRegionKind) : Region
• Erased : Region
• Error : Region

def Miri.MIR.instReprRegion.repr : Region → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instReprRegion.repr Miri.MIR.Region.Static prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.Region.Static")).group prec✝
• Miri.MIR.instReprRegion.repr Miri.MIR.Region.Erased prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.Region.Erased")).group prec✝
• Miri.MIR.instReprRegion.repr Miri.MIR.Region.Error prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.Region.Error")).group prec✝

@[instance_reducible]

instance Miri.MIR.instReprRegion : Repr Region

Equations

• Miri.MIR.instReprRegion = { reprPrec := Miri.MIR.instReprRegion.repr }

def Miri.MIR.instDecidableEqRegion.decEq (x✝ x✝¹ : Region) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.EarlyParameter index name) (Miri.MIR.Region.Bound indexKind variableIndex kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.EarlyParameter index name) (Miri.MIR.Region.LateParameter scope kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.EarlyParameter index name) Miri.MIR.Region.Static = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.EarlyParameter index name) (Miri.MIR.Region.InferenceVariable index_1) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.EarlyParameter index name) (Miri.MIR.Region.Placeholder universeIndex variableIndex kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.EarlyParameter index name) Miri.MIR.Region.Erased = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.EarlyParameter index name) Miri.MIR.Region.Error = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.Bound indexKind variableIndex kind) (Miri.MIR.Region.EarlyParameter index name) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.Bound indexKind variableIndex kind) (Miri.MIR.Region.LateParameter scope kind_1) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.Bound indexKind variableIndex kind) Miri.MIR.Region.Static = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.Bound indexKind variableIndex kind) (Miri.MIR.Region.InferenceVariable index) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.Bound indexKind variableIndex kind) (Miri.MIR.Region.Placeholder universeIndex variableIndex_1 kind_1) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.Bound indexKind variableIndex kind) Miri.MIR.Region.Erased = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.Bound indexKind variableIndex kind) Miri.MIR.Region.Error = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.LateParameter scope kind) (Miri.MIR.Region.EarlyParameter index name) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.LateParameter scope kind) (Miri.MIR.Region.Bound indexKind variableIndex kind_1) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.LateParameter scope kind) Miri.MIR.Region.Static = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.LateParameter scope kind) (Miri.MIR.Region.InferenceVariable index) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.LateParameter scope kind) (Miri.MIR.Region.Placeholder universeIndex variableIndex kind_1) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.LateParameter scope kind) Miri.MIR.Region.Erased = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.LateParameter scope kind) Miri.MIR.Region.Error = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Static (Miri.MIR.Region.EarlyParameter index name) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Static (Miri.MIR.Region.Bound indexKind variableIndex kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Static (Miri.MIR.Region.LateParameter scope kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Static Miri.MIR.Region.Static = isTrue ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Static (Miri.MIR.Region.InferenceVariable index) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Static (Miri.MIR.Region.Placeholder universeIndex variableIndex kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Static Miri.MIR.Region.Erased = isFalse Miri.MIR.instDecidableEqRegion.decEq._proof_37
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Static Miri.MIR.Region.Error = isFalse Miri.MIR.instDecidableEqRegion.decEq._proof_38
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.InferenceVariable index) (Miri.MIR.Region.EarlyParameter index_1 name) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.InferenceVariable index) (Miri.MIR.Region.Bound indexKind variableIndex kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.InferenceVariable index) (Miri.MIR.Region.LateParameter scope kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.InferenceVariable index) Miri.MIR.Region.Static = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.InferenceVariable a) (Miri.MIR.Region.InferenceVariable b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.InferenceVariable index) (Miri.MIR.Region.Placeholder universeIndex variableIndex kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.InferenceVariable index) Miri.MIR.Region.Erased = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.InferenceVariable index) Miri.MIR.Region.Error = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.Placeholder universeIndex variableIndex kind) (Miri.MIR.Region.EarlyParameter index name) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.Placeholder universeIndex variableIndex kind) (Miri.MIR.Region.Bound indexKind variableIndex_1 kind_1) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.Placeholder universeIndex variableIndex kind) (Miri.MIR.Region.LateParameter scope kind_1) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.Placeholder universeIndex variableIndex kind) Miri.MIR.Region.Static = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.Placeholder universeIndex variableIndex kind) (Miri.MIR.Region.InferenceVariable index) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.Placeholder universeIndex variableIndex kind) Miri.MIR.Region.Erased = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq (Miri.MIR.Region.Placeholder universeIndex variableIndex kind) Miri.MIR.Region.Error = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Erased (Miri.MIR.Region.EarlyParameter index name) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Erased (Miri.MIR.Region.Bound indexKind variableIndex kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Erased (Miri.MIR.Region.LateParameter scope kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Erased Miri.MIR.Region.Static = isFalse Miri.MIR.instDecidableEqRegion.decEq._proof_62
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Erased (Miri.MIR.Region.InferenceVariable index) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Erased (Miri.MIR.Region.Placeholder universeIndex variableIndex kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Erased Miri.MIR.Region.Erased = isTrue ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Erased Miri.MIR.Region.Error = isFalse Miri.MIR.instDecidableEqRegion.decEq._proof_65
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Error (Miri.MIR.Region.EarlyParameter index name) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Error (Miri.MIR.Region.Bound indexKind variableIndex kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Error (Miri.MIR.Region.LateParameter scope kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Error Miri.MIR.Region.Static = isFalse Miri.MIR.instDecidableEqRegion.decEq._proof_69
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Error (Miri.MIR.Region.InferenceVariable index) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Error (Miri.MIR.Region.Placeholder universeIndex variableIndex kind) = isFalse ⋯
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Error Miri.MIR.Region.Erased = isFalse Miri.MIR.instDecidableEqRegion.decEq._proof_72
• Miri.MIR.instDecidableEqRegion.decEq Miri.MIR.Region.Error Miri.MIR.Region.Error = isTrue ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqRegion : DecidableEq Region

Equations

• Miri.MIR.instDecidableEqRegion = Miri.MIR.instDecidableEqRegion.decEq

inductive Miri.MIR.GenericArg : Type

• Type (ty : TyId) : GenericArg
• Lifetime (region : Region) : GenericArg
• Const (value : TypeConstId) : GenericArg

@[instance_reducible]

instance Miri.MIR.instReprGenericArg : Repr GenericArg

Equations

• Miri.MIR.instReprGenericArg = { reprPrec := Miri.MIR.instReprGenericArg.repr }

def Miri.MIR.instReprGenericArg.repr : GenericArg → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqGenericArg : DecidableEq GenericArg

Equations

• Miri.MIR.instDecidableEqGenericArg = Miri.MIR.instDecidableEqGenericArg.decEq

def Miri.MIR.instDecidableEqGenericArg.decEq (x✝ x✝¹ : GenericArg) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqGenericArg.decEq (Miri.MIR.GenericArg.Type a) (Miri.MIR.GenericArg.Type b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqGenericArg.decEq (Miri.MIR.GenericArg.Type ty) (Miri.MIR.GenericArg.Lifetime region) = isFalse ⋯
• Miri.MIR.instDecidableEqGenericArg.decEq (Miri.MIR.GenericArg.Type ty) (Miri.MIR.GenericArg.Const value) = isFalse ⋯
• Miri.MIR.instDecidableEqGenericArg.decEq (Miri.MIR.GenericArg.Lifetime region) (Miri.MIR.GenericArg.Type ty) = isFalse ⋯
• Miri.MIR.instDecidableEqGenericArg.decEq (Miri.MIR.GenericArg.Lifetime a) (Miri.MIR.GenericArg.Lifetime b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqGenericArg.decEq (Miri.MIR.GenericArg.Lifetime region) (Miri.MIR.GenericArg.Const value) = isFalse ⋯
• Miri.MIR.instDecidableEqGenericArg.decEq (Miri.MIR.GenericArg.Const value) (Miri.MIR.GenericArg.Type ty) = isFalse ⋯
• Miri.MIR.instDecidableEqGenericArg.decEq (Miri.MIR.GenericArg.Const value) (Miri.MIR.GenericArg.Lifetime region) = isFalse ⋯
• Miri.MIR.instDecidableEqGenericArg.decEq (Miri.MIR.GenericArg.Const a) (Miri.MIR.GenericArg.Const b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.ValTreeNode : Type

• Leaf (bits sizeBytes : Nat) : ValTreeNode
• Branch (fields : Array TypeConstId) : ValTreeNode

def Miri.MIR.instReprValTreeNode.repr : ValTreeNode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprValTreeNode : Repr ValTreeNode

Equations

• Miri.MIR.instReprValTreeNode = { reprPrec := Miri.MIR.instReprValTreeNode.repr }

def Miri.MIR.instDecidableEqValTreeNode.decEq (x✝ x✝¹ : ValTreeNode) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqValTreeNode.decEq (Miri.MIR.ValTreeNode.Leaf bits sizeBytes) (Miri.MIR.ValTreeNode.Branch fields) = isFalse ⋯
• Miri.MIR.instDecidableEqValTreeNode.decEq (Miri.MIR.ValTreeNode.Branch fields) (Miri.MIR.ValTreeNode.Leaf bits sizeBytes) = isFalse ⋯
• Miri.MIR.instDecidableEqValTreeNode.decEq (Miri.MIR.ValTreeNode.Branch a) (Miri.MIR.ValTreeNode.Branch b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqValTreeNode : DecidableEq ValTreeNode

Equations

• Miri.MIR.instDecidableEqValTreeNode = Miri.MIR.instDecidableEqValTreeNode.decEq

structure Miri.MIR.ValTree : Type

• nodes : Array ValTreeNode
• root : Nat

@[instance_reducible]

instance Miri.MIR.instReprValTree : Repr ValTree

Equations

• Miri.MIR.instReprValTree = { reprPrec := Miri.MIR.instReprValTree.repr }

def Miri.MIR.instReprValTree.repr : ValTree → Nat → Std.Format

Equations

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

def Miri.MIR.instDecidableEqValTree.decEq (x✝ x✝¹ : ValTree) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqValTree.decEq { nodes := a, root := a_1 } { nodes := b, root := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqValTree : DecidableEq ValTree

Equations

• Miri.MIR.instDecidableEqValTree = Miri.MIR.instDecidableEqValTree.decEq

inductive Miri.MIR.TypeConst : Type

• Param (index : Nat) (name : String) (declaredType : Option TyId) : TypeConst
• InferVar (id : Nat) : TypeConst
• InferFresh (id : Nat) : TypeConst
• Bound (indexKind : BoundVarIndexKind) (variableIndex : Nat) : TypeConst
• Placeholder (universeIndex variableIndex : Nat) : TypeConst
• Alias (rigid : Bool) (kind : ConstAliasKind) (definition : DefId) (arguments : Array GenericArg) : TypeConst
• Value (ty : TyId) (tree : ValTree) : TypeConst
• Error : TypeConst
• Expr (kind : ConstExpressionKind) (arguments : Array GenericArg) : TypeConst

def Miri.MIR.instReprTypeConst.repr : TypeConst → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instReprTypeConst.repr Miri.MIR.TypeConst.Error prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.TypeConst.Error")).group prec✝

@[instance_reducible]

instance Miri.MIR.instReprTypeConst : Repr TypeConst

Equations

• Miri.MIR.instReprTypeConst = { reprPrec := Miri.MIR.instReprTypeConst.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqTypeConst : DecidableEq TypeConst

Equations

• Miri.MIR.instDecidableEqTypeConst = Miri.MIR.instDecidableEqTypeConst.decEq

def Miri.MIR.instDecidableEqTypeConst.decEq (x✝ x✝¹ : TypeConst) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Param index name declaredType) (Miri.MIR.TypeConst.InferVar id) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Param index name declaredType) (Miri.MIR.TypeConst.InferFresh id) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Param index name declaredType) (Miri.MIR.TypeConst.Bound indexKind variableIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Param index name declaredType) (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Param index name declaredType) (Miri.MIR.TypeConst.Alias rigid kind definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Param index name declaredType) (Miri.MIR.TypeConst.Value ty tree) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Param index name declaredType) Miri.MIR.TypeConst.Error = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Param index name declaredType) (Miri.MIR.TypeConst.Expr kind arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferVar id) (Miri.MIR.TypeConst.Param index name declaredType) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferVar a) (Miri.MIR.TypeConst.InferVar b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferVar id) (Miri.MIR.TypeConst.InferFresh id_1) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferVar id) (Miri.MIR.TypeConst.Bound indexKind variableIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferVar id) (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferVar id) (Miri.MIR.TypeConst.Alias rigid kind definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferVar id) (Miri.MIR.TypeConst.Value ty tree) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferVar id) Miri.MIR.TypeConst.Error = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferVar id) (Miri.MIR.TypeConst.Expr kind arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferFresh id) (Miri.MIR.TypeConst.Param index name declaredType) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferFresh id) (Miri.MIR.TypeConst.InferVar id_1) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferFresh a) (Miri.MIR.TypeConst.InferFresh b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferFresh id) (Miri.MIR.TypeConst.Bound indexKind variableIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferFresh id) (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferFresh id) (Miri.MIR.TypeConst.Alias rigid kind definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferFresh id) (Miri.MIR.TypeConst.Value ty tree) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferFresh id) Miri.MIR.TypeConst.Error = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.InferFresh id) (Miri.MIR.TypeConst.Expr kind arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Bound indexKind variableIndex) (Miri.MIR.TypeConst.Param index name declaredType) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Bound indexKind variableIndex) (Miri.MIR.TypeConst.InferVar id) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Bound indexKind variableIndex) (Miri.MIR.TypeConst.InferFresh id) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Bound a a_1) (Miri.MIR.TypeConst.Bound b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Bound indexKind variableIndex) (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex_1) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Bound indexKind variableIndex) (Miri.MIR.TypeConst.Alias rigid kind definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Bound indexKind variableIndex) (Miri.MIR.TypeConst.Value ty tree) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Bound indexKind variableIndex) Miri.MIR.TypeConst.Error = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Bound indexKind variableIndex) (Miri.MIR.TypeConst.Expr kind arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) (Miri.MIR.TypeConst.Param index name declaredType) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) (Miri.MIR.TypeConst.InferVar id) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) (Miri.MIR.TypeConst.InferFresh id) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) (Miri.MIR.TypeConst.Bound indexKind variableIndex_1) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) (Miri.MIR.TypeConst.Alias rigid kind definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) (Miri.MIR.TypeConst.Value ty tree) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) Miri.MIR.TypeConst.Error = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) (Miri.MIR.TypeConst.Expr kind arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Alias rigid kind definition arguments) (Miri.MIR.TypeConst.Param index name declaredType) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Alias rigid kind definition arguments) (Miri.MIR.TypeConst.InferVar id) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Alias rigid kind definition arguments) (Miri.MIR.TypeConst.InferFresh id) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Alias rigid kind definition arguments) (Miri.MIR.TypeConst.Bound indexKind variableIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Alias rigid kind definition arguments) (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Alias rigid kind definition arguments) (Miri.MIR.TypeConst.Value ty tree) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Alias rigid kind definition arguments) Miri.MIR.TypeConst.Error = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Alias rigid kind definition arguments) (Miri.MIR.TypeConst.Expr kind_1 arguments_1) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Value ty tree) (Miri.MIR.TypeConst.Param index name declaredType) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Value ty tree) (Miri.MIR.TypeConst.InferVar id) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Value ty tree) (Miri.MIR.TypeConst.InferFresh id) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Value ty tree) (Miri.MIR.TypeConst.Bound indexKind variableIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Value ty tree) (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Value ty tree) (Miri.MIR.TypeConst.Alias rigid kind definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Value a a_1) (Miri.MIR.TypeConst.Value b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Value ty tree) Miri.MIR.TypeConst.Error = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Value ty tree) (Miri.MIR.TypeConst.Expr kind arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq Miri.MIR.TypeConst.Error (Miri.MIR.TypeConst.Param index name declaredType) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq Miri.MIR.TypeConst.Error (Miri.MIR.TypeConst.InferVar id) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq Miri.MIR.TypeConst.Error (Miri.MIR.TypeConst.InferFresh id) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq Miri.MIR.TypeConst.Error (Miri.MIR.TypeConst.Bound indexKind variableIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq Miri.MIR.TypeConst.Error (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq Miri.MIR.TypeConst.Error (Miri.MIR.TypeConst.Alias rigid kind definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq Miri.MIR.TypeConst.Error (Miri.MIR.TypeConst.Value ty tree) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq Miri.MIR.TypeConst.Error Miri.MIR.TypeConst.Error = isTrue ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq Miri.MIR.TypeConst.Error (Miri.MIR.TypeConst.Expr kind arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Expr kind arguments) (Miri.MIR.TypeConst.Param index name declaredType) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Expr kind arguments) (Miri.MIR.TypeConst.InferVar id) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Expr kind arguments) (Miri.MIR.TypeConst.InferFresh id) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Expr kind arguments) (Miri.MIR.TypeConst.Bound indexKind variableIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Expr kind arguments) (Miri.MIR.TypeConst.Placeholder universeIndex variableIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Expr kind arguments) (Miri.MIR.TypeConst.Alias rigid kind_1 definition arguments_1) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Expr kind arguments) (Miri.MIR.TypeConst.Value ty tree) = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Expr kind arguments) Miri.MIR.TypeConst.Error = isFalse ⋯
• Miri.MIR.instDecidableEqTypeConst.decEq (Miri.MIR.TypeConst.Expr a a_1) (Miri.MIR.TypeConst.Expr b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

structure Miri.MIR.UnevaluatedConst : Type

• definition : DefId
• arguments : Array GenericArg
• promoted : Option Nat

@[instance_reducible]

instance Miri.MIR.instReprUnevaluatedConst : Repr UnevaluatedConst

Equations

• Miri.MIR.instReprUnevaluatedConst = { reprPrec := Miri.MIR.instReprUnevaluatedConst.repr }

def Miri.MIR.instReprUnevaluatedConst.repr : UnevaluatedConst → Nat → Std.Format

Equations

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

def Miri.MIR.instDecidableEqUnevaluatedConst.decEq (x✝ x✝¹ : UnevaluatedConst) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqUnevaluatedConst : DecidableEq UnevaluatedConst

Equations

• Miri.MIR.instDecidableEqUnevaluatedConst = Miri.MIR.instDecidableEqUnevaluatedConst.decEq

inductive Miri.MIR.MirConst : Type

• Ty (ty : TyId) (value : TypeConst) : MirConst
• Unevaluated (constant : UnevaluatedConst) (ty : TyId) : MirConst
• Val (value : ConstValue) (ty : TyId) : MirConst

def Miri.MIR.instReprMirConst.repr : MirConst → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprMirConst : Repr MirConst

Equations

• Miri.MIR.instReprMirConst = { reprPrec := Miri.MIR.instReprMirConst.repr }

def Miri.MIR.instDecidableEqMirConst.decEq (x✝ x✝¹ : MirConst) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqMirConst.decEq (Miri.MIR.MirConst.Ty a a_1) (Miri.MIR.MirConst.Ty b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqMirConst.decEq (Miri.MIR.MirConst.Ty ty value) (Miri.MIR.MirConst.Unevaluated constant ty_1) = isFalse ⋯
• Miri.MIR.instDecidableEqMirConst.decEq (Miri.MIR.MirConst.Ty ty value) (Miri.MIR.MirConst.Val value_1 ty_1) = isFalse ⋯
• Miri.MIR.instDecidableEqMirConst.decEq (Miri.MIR.MirConst.Unevaluated constant ty) (Miri.MIR.MirConst.Ty ty_1 value) = isFalse ⋯
• Miri.MIR.instDecidableEqMirConst.decEq (Miri.MIR.MirConst.Unevaluated constant ty) (Miri.MIR.MirConst.Val value ty_1) = isFalse ⋯
• Miri.MIR.instDecidableEqMirConst.decEq (Miri.MIR.MirConst.Val value ty) (Miri.MIR.MirConst.Ty ty_1 value_1) = isFalse ⋯
• Miri.MIR.instDecidableEqMirConst.decEq (Miri.MIR.MirConst.Val value ty) (Miri.MIR.MirConst.Unevaluated constant ty_1) = isFalse ⋯
• Miri.MIR.instDecidableEqMirConst.decEq (Miri.MIR.MirConst.Val a a_1) (Miri.MIR.MirConst.Val b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqMirConst : DecidableEq MirConst

Equations

• Miri.MIR.instDecidableEqMirConst = Miri.MIR.instDecidableEqMirConst.decEq

structure Miri.MIR.ConstOperand : Type

• span : SpanRef
• userType : Option UserTypeAnnotationIndex
• value : MirConst

def Miri.MIR.instReprConstOperand.repr : ConstOperand → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprConstOperand : Repr ConstOperand

Equations

• Miri.MIR.instReprConstOperand = { reprPrec := Miri.MIR.instReprConstOperand.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqConstOperand : DecidableEq ConstOperand

Equations

• Miri.MIR.instDecidableEqConstOperand = Miri.MIR.instDecidableEqConstOperand.decEq

def Miri.MIR.instDecidableEqConstOperand.decEq (x✝ x✝¹ : ConstOperand) : Decidable (x✝ = x✝¹)

Equations

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

inductive Miri.MIR.ProjectionElem : Type

• Deref : ProjectionElem
• Field (field : FieldIndex) (ty : TyId) : ProjectionElem
• Index (localId : LocalId) : ProjectionElem
• ConstantIndex (offset minLength : Nat) (fromEnd : Bool) : ProjectionElem
• Subslice (fromIndex toIndex : Nat) (fromEnd : Bool) : ProjectionElem
• Downcast (name : Option String) (variant : VariantIndex) : ProjectionElem
• OpaqueCast (ty : TyId) : ProjectionElem
• UnwrapUnsafeBinder (ty : TyId) : ProjectionElem
• PhantomDeref : ProjectionElem

def Miri.MIR.instReprProjectionElem.repr : ProjectionElem → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprProjectionElem : Repr ProjectionElem

Equations

• Miri.MIR.instReprProjectionElem = { reprPrec := Miri.MIR.instReprProjectionElem.repr }

def Miri.MIR.instDecidableEqProjectionElem.decEq (x✝ x✝¹ : ProjectionElem) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.Deref Miri.MIR.ProjectionElem.Deref = isTrue ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.Deref (Miri.MIR.ProjectionElem.Field field ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.Deref (Miri.MIR.ProjectionElem.Index localId) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.Deref (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.Deref (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.Deref (Miri.MIR.ProjectionElem.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.Deref (Miri.MIR.ProjectionElem.OpaqueCast ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.Deref (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.Deref Miri.MIR.ProjectionElem.PhantomDeref = isFalse Miri.MIR.instDecidableEqProjectionElem.decEq._proof_8
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Field field ty) Miri.MIR.ProjectionElem.Deref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Field field ty) (Miri.MIR.ProjectionElem.Index localId) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Field field ty) (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Field field ty) (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Field field ty) (Miri.MIR.ProjectionElem.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Field field ty) (Miri.MIR.ProjectionElem.OpaqueCast ty_1) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Field field ty) (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty_1) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Field field ty) Miri.MIR.ProjectionElem.PhantomDeref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Index localId) Miri.MIR.ProjectionElem.Deref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Index localId) (Miri.MIR.ProjectionElem.Field field ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Index a) (Miri.MIR.ProjectionElem.Index b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Index localId) (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Index localId) (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Index localId) (Miri.MIR.ProjectionElem.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Index localId) (Miri.MIR.ProjectionElem.OpaqueCast ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Index localId) (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Index localId) Miri.MIR.ProjectionElem.PhantomDeref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) Miri.MIR.ProjectionElem.Deref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) (Miri.MIR.ProjectionElem.Field field ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) (Miri.MIR.ProjectionElem.Index localId) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd_1) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) (Miri.MIR.ProjectionElem.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) (Miri.MIR.ProjectionElem.OpaqueCast ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) Miri.MIR.ProjectionElem.PhantomDeref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) Miri.MIR.ProjectionElem.Deref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) (Miri.MIR.ProjectionElem.Field field ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) (Miri.MIR.ProjectionElem.Index localId) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd_1) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) (Miri.MIR.ProjectionElem.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) (Miri.MIR.ProjectionElem.OpaqueCast ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) Miri.MIR.ProjectionElem.PhantomDeref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Downcast name variant) Miri.MIR.ProjectionElem.Deref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Downcast name variant) (Miri.MIR.ProjectionElem.Field field ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Downcast name variant) (Miri.MIR.ProjectionElem.Index localId) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Downcast name variant) (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Downcast name variant) (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Downcast name variant) (Miri.MIR.ProjectionElem.OpaqueCast ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Downcast name variant) (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.Downcast name variant) Miri.MIR.ProjectionElem.PhantomDeref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.OpaqueCast ty) Miri.MIR.ProjectionElem.Deref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.OpaqueCast ty) (Miri.MIR.ProjectionElem.Field field ty_1) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.OpaqueCast ty) (Miri.MIR.ProjectionElem.Index localId) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.OpaqueCast ty) (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.OpaqueCast ty) (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.OpaqueCast ty) (Miri.MIR.ProjectionElem.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.OpaqueCast a) (Miri.MIR.ProjectionElem.OpaqueCast b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.OpaqueCast ty) (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty_1) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.OpaqueCast ty) Miri.MIR.ProjectionElem.PhantomDeref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) Miri.MIR.ProjectionElem.Deref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) (Miri.MIR.ProjectionElem.Field field ty_1) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) (Miri.MIR.ProjectionElem.Index localId) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) (Miri.MIR.ProjectionElem.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) (Miri.MIR.ProjectionElem.OpaqueCast ty_1) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder a) (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) Miri.MIR.ProjectionElem.PhantomDeref = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.PhantomDeref Miri.MIR.ProjectionElem.Deref = isFalse Miri.MIR.instDecidableEqProjectionElem.decEq._proof_85
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.PhantomDeref (Miri.MIR.ProjectionElem.Field field ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.PhantomDeref (Miri.MIR.ProjectionElem.Index localId) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.PhantomDeref (Miri.MIR.ProjectionElem.ConstantIndex offset minLength fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.PhantomDeref (Miri.MIR.ProjectionElem.Subslice fromIndex toIndex fromEnd) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.PhantomDeref (Miri.MIR.ProjectionElem.Downcast name variant) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.PhantomDeref (Miri.MIR.ProjectionElem.OpaqueCast ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.PhantomDeref (Miri.MIR.ProjectionElem.UnwrapUnsafeBinder ty) = isFalse ⋯
• Miri.MIR.instDecidableEqProjectionElem.decEq Miri.MIR.ProjectionElem.PhantomDeref Miri.MIR.ProjectionElem.PhantomDeref = isTrue ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqProjectionElem : DecidableEq ProjectionElem

Equations

• Miri.MIR.instDecidableEqProjectionElem = Miri.MIR.instDecidableEqProjectionElem.decEq

structure Miri.MIR.Place : Type

• localId : LocalId
• projection : Array ProjectionElem

@[instance_reducible]

instance Miri.MIR.instReprPlace : Repr Place

Equations

• Miri.MIR.instReprPlace = { reprPrec := Miri.MIR.instReprPlace.repr }

def Miri.MIR.instReprPlace.repr : Place → Nat → Std.Format

Equations

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

def Miri.MIR.instDecidableEqPlace.decEq (x✝ x✝¹ : Place) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqPlace.decEq { localId := a, projection := a_1 } { localId := b, projection := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqPlace : DecidableEq Place

Equations

• Miri.MIR.instDecidableEqPlace = Miri.MIR.instDecidableEqPlace.decEq

inductive Miri.MIR.Operand : Type

• Copy (place : Place) : Operand
• Move (place : Place) : Operand
• Constant (constant : ConstOperand) : Operand
• RuntimeChecks (check : MIR.RuntimeChecks) : Operand

def Miri.MIR.instReprOperand.repr : Operand → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprOperand : Repr Operand

Equations

• Miri.MIR.instReprOperand = { reprPrec := Miri.MIR.instReprOperand.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqOperand : DecidableEq Operand

Equations

• Miri.MIR.instDecidableEqOperand = Miri.MIR.instDecidableEqOperand.decEq

def Miri.MIR.instDecidableEqOperand.decEq (x✝ x✝¹ : Operand) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.Copy a) (Miri.MIR.Operand.Copy b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.Copy place) (Miri.MIR.Operand.Move place_1) = isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.Copy place) (Miri.MIR.Operand.Constant constant) = isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.Copy place) (Miri.MIR.Operand.RuntimeChecks check) = isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.Move place) (Miri.MIR.Operand.Copy place_1) = isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.Move a) (Miri.MIR.Operand.Move b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.Move place) (Miri.MIR.Operand.Constant constant) = isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.Move place) (Miri.MIR.Operand.RuntimeChecks check) = isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.Constant constant) (Miri.MIR.Operand.Copy place) = isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.Constant constant) (Miri.MIR.Operand.Move place) = isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.Constant a) (Miri.MIR.Operand.Constant b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.Constant constant) (Miri.MIR.Operand.RuntimeChecks check) = isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.RuntimeChecks check) (Miri.MIR.Operand.Copy place) = isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.RuntimeChecks check) (Miri.MIR.Operand.Move place) = isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.RuntimeChecks check) (Miri.MIR.Operand.Constant constant) = isFalse ⋯
• Miri.MIR.instDecidableEqOperand.decEq (Miri.MIR.Operand.RuntimeChecks a) (Miri.MIR.Operand.RuntimeChecks b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

structure Miri.MIR.CopyNonOverlapping : Type

• source : Operand
• destination : Operand
• count : Operand

@[instance_reducible]

instance Miri.MIR.instReprCopyNonOverlapping : Repr CopyNonOverlapping

Equations

• Miri.MIR.instReprCopyNonOverlapping = { reprPrec := Miri.MIR.instReprCopyNonOverlapping.repr }

def Miri.MIR.instReprCopyNonOverlapping.repr : CopyNonOverlapping → Nat → Std.Format

Equations

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

def Miri.MIR.instDecidableEqCopyNonOverlapping.decEq (x✝ x✝¹ : CopyNonOverlapping) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqCopyNonOverlapping : DecidableEq CopyNonOverlapping

Equations

• Miri.MIR.instDecidableEqCopyNonOverlapping = Miri.MIR.instDecidableEqCopyNonOverlapping.decEq

inductive Miri.MIR.NonDivergingIntrinsic : Type

• Assume (condition : Operand) : NonDivergingIntrinsic
• CopyNonOverlapping (args : MIR.CopyNonOverlapping) : NonDivergingIntrinsic

@[instance_reducible]

instance Miri.MIR.instReprNonDivergingIntrinsic : Repr NonDivergingIntrinsic

Equations

• Miri.MIR.instReprNonDivergingIntrinsic = { reprPrec := Miri.MIR.instReprNonDivergingIntrinsic.repr }

def Miri.MIR.instReprNonDivergingIntrinsic.repr : NonDivergingIntrinsic → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqNonDivergingIntrinsic : DecidableEq NonDivergingIntrinsic

Equations

• Miri.MIR.instDecidableEqNonDivergingIntrinsic = Miri.MIR.instDecidableEqNonDivergingIntrinsic.decEq

def Miri.MIR.instDecidableEqNonDivergingIntrinsic.decEq (x✝ x✝¹ : NonDivergingIntrinsic) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqNonDivergingIntrinsic.decEq (Miri.MIR.NonDivergingIntrinsic.Assume a) (Miri.MIR.NonDivergingIntrinsic.Assume b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqNonDivergingIntrinsic.decEq (Miri.MIR.NonDivergingIntrinsic.Assume condition) (Miri.MIR.NonDivergingIntrinsic.CopyNonOverlapping args) = isFalse ⋯
• Miri.MIR.instDecidableEqNonDivergingIntrinsic.decEq (Miri.MIR.NonDivergingIntrinsic.CopyNonOverlapping args) (Miri.MIR.NonDivergingIntrinsic.Assume condition) = isFalse ⋯

inductive Miri.MIR.AggregateKind : Type

• Array (elementType : TyId) : AggregateKind
• Tuple : AggregateKind
• Adt (definition : DefId) (variant : VariantIndex) (arguments : _root_.Array GenericArg) (userType : Option UserTypeAnnotationIndex) (activeField : Option FieldIndex) : AggregateKind
• Closure (definition : DefId) (arguments : _root_.Array GenericArg) : AggregateKind
• Coroutine (definition : DefId) (arguments : _root_.Array GenericArg) : AggregateKind
• CoroutineClosure (definition : DefId) (arguments : _root_.Array GenericArg) : AggregateKind
• RawPtr (pointeeType : TyId) (mutability : Mutability) : AggregateKind

@[instance_reducible]

instance Miri.MIR.instReprAggregateKind : Repr AggregateKind

Equations

• Miri.MIR.instReprAggregateKind = { reprPrec := Miri.MIR.instReprAggregateKind.repr }

def Miri.MIR.instReprAggregateKind.repr : AggregateKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqAggregateKind : DecidableEq AggregateKind

Equations

• Miri.MIR.instDecidableEqAggregateKind = Miri.MIR.instDecidableEqAggregateKind.decEq

def Miri.MIR.instDecidableEqAggregateKind.decEq (x✝ x✝¹ : AggregateKind) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Array a) (Miri.MIR.AggregateKind.Array b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Array elementType) Miri.MIR.AggregateKind.Tuple = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Array elementType) (Miri.MIR.AggregateKind.Adt definition variant arguments userType activeField) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Array elementType) (Miri.MIR.AggregateKind.Closure definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Array elementType) (Miri.MIR.AggregateKind.Coroutine definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Array elementType) (Miri.MIR.AggregateKind.CoroutineClosure definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Array elementType) (Miri.MIR.AggregateKind.RawPtr pointeeType mutability) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq Miri.MIR.AggregateKind.Tuple (Miri.MIR.AggregateKind.Array elementType) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq Miri.MIR.AggregateKind.Tuple Miri.MIR.AggregateKind.Tuple = isTrue ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq Miri.MIR.AggregateKind.Tuple (Miri.MIR.AggregateKind.Adt definition variant arguments userType activeField) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq Miri.MIR.AggregateKind.Tuple (Miri.MIR.AggregateKind.Closure definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq Miri.MIR.AggregateKind.Tuple (Miri.MIR.AggregateKind.Coroutine definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq Miri.MIR.AggregateKind.Tuple (Miri.MIR.AggregateKind.CoroutineClosure definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq Miri.MIR.AggregateKind.Tuple (Miri.MIR.AggregateKind.RawPtr pointeeType mutability) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Adt definition variant arguments userType activeField) (Miri.MIR.AggregateKind.Array elementType) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Adt definition variant arguments userType activeField) Miri.MIR.AggregateKind.Tuple = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Adt definition variant arguments userType activeField) (Miri.MIR.AggregateKind.RawPtr pointeeType mutability) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Closure definition arguments) (Miri.MIR.AggregateKind.Array elementType) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Closure definition arguments) Miri.MIR.AggregateKind.Tuple = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Closure definition arguments) (Miri.MIR.AggregateKind.Adt definition_1 variant arguments_1 userType activeField) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Closure definition arguments) (Miri.MIR.AggregateKind.Coroutine definition_1 arguments_1) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Closure definition arguments) (Miri.MIR.AggregateKind.CoroutineClosure definition_1 arguments_1) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Closure definition arguments) (Miri.MIR.AggregateKind.RawPtr pointeeType mutability) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Coroutine definition arguments) (Miri.MIR.AggregateKind.Array elementType) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Coroutine definition arguments) Miri.MIR.AggregateKind.Tuple = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Coroutine definition arguments) (Miri.MIR.AggregateKind.Closure definition_1 arguments_1) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Coroutine definition arguments) (Miri.MIR.AggregateKind.CoroutineClosure definition_1 arguments_1) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.Coroutine definition arguments) (Miri.MIR.AggregateKind.RawPtr pointeeType mutability) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.CoroutineClosure definition arguments) (Miri.MIR.AggregateKind.Array elementType) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.CoroutineClosure definition arguments) Miri.MIR.AggregateKind.Tuple = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.CoroutineClosure definition arguments) (Miri.MIR.AggregateKind.Closure definition_1 arguments_1) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.CoroutineClosure definition arguments) (Miri.MIR.AggregateKind.Coroutine definition_1 arguments_1) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.CoroutineClosure definition arguments) (Miri.MIR.AggregateKind.RawPtr pointeeType mutability) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.RawPtr pointeeType mutability) (Miri.MIR.AggregateKind.Array elementType) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.RawPtr pointeeType mutability) Miri.MIR.AggregateKind.Tuple = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.RawPtr pointeeType mutability) (Miri.MIR.AggregateKind.Adt definition variant arguments userType activeField) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.RawPtr pointeeType mutability) (Miri.MIR.AggregateKind.Closure definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.RawPtr pointeeType mutability) (Miri.MIR.AggregateKind.Coroutine definition arguments) = isFalse ⋯
• Miri.MIR.instDecidableEqAggregateKind.decEq (Miri.MIR.AggregateKind.RawPtr pointeeType mutability) (Miri.MIR.AggregateKind.CoroutineClosure definition arguments) = isFalse ⋯

inductive Miri.MIR.Rvalue : Type

• Use (operand : Operand) (retag : WithRetag) : Rvalue
• Repeat (operand : Operand) (count : TypeConst) : Rvalue
• Ref (region : Region) (borrow : BorrowKind) (place : Place) : Rvalue
• ThreadLocalRef (definition : DefId) : Rvalue
• RawPtr (kind : RawPtrKind) (place : Place) : Rvalue
• Cast (kind : CastKind) (operand : Operand) (targetType : TyId) : Rvalue
• BinaryOp (operator : BinOp) (left right : Operand) : Rvalue
• UnaryOp (operator : UnOp) (operand : Operand) : Rvalue
• Discriminant (place : Place) : Rvalue
• Aggregate (kind : AggregateKind) (operands : Array Operand) : Rvalue
• CopyForDeref (place : Place) : Rvalue
• WrapUnsafeBinder (operand : Operand) (targetType : TyId) : Rvalue
• Reborrow (ty : TyId) (mutability : Mutability) (place : Place) : Rvalue

@[instance_reducible]

instance Miri.MIR.instReprRvalue : Repr Rvalue

Equations

• Miri.MIR.instReprRvalue = { reprPrec := Miri.MIR.instReprRvalue.repr }

def Miri.MIR.instReprRvalue.repr : Rvalue → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqRvalue : DecidableEq Rvalue

Equations

• Miri.MIR.instDecidableEqRvalue = Miri.MIR.instDecidableEqRvalue.decEq

def Miri.MIR.instDecidableEqRvalue.decEq (x✝ x✝¹ : Rvalue) : Decidable (x✝ = x✝¹)

Equations

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

inductive Miri.MIR.StatementKind : Type

• Assign (destination : Place) (value : Rvalue) : StatementKind
• FakeRead (cause : FakeReadCause) (place : Place) : StatementKind
• SetDiscriminant (place : Place) (variant : VariantIndex) : StatementKind
• StorageLive (localId : LocalId) : StatementKind
• StorageDead (localId : LocalId) : StatementKind
• PlaceMention (place : Place) : StatementKind
• AscribeUserType (place : Place) (projection : UserTypeProjection) (variance : Variance) : StatementKind
• Coverage (coverage : CoverageKind) : StatementKind
• Intrinsic (intrinsic : NonDivergingIntrinsic) : StatementKind
• ConstEvalCounter : StatementKind
• Nop : StatementKind
• BackwardIncompatibleDropHint (place : Place) (reason : BackwardIncompatibleDropReason) : StatementKind

@[instance_reducible]

instance Miri.MIR.instReprStatementKind : Repr StatementKind

Equations

• Miri.MIR.instReprStatementKind = { reprPrec := Miri.MIR.instReprStatementKind.repr }

def Miri.MIR.instReprStatementKind.repr : StatementKind → Nat → Std.Format

Equations

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

def Miri.MIR.instDecidableEqStatementKind.decEq (x✝ x✝¹ : StatementKind) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqStatementKind : DecidableEq StatementKind

Equations

• Miri.MIR.instDecidableEqStatementKind = Miri.MIR.instDecidableEqStatementKind.decEq

inductive Miri.MIR.SwitchTarget : Type

• Case (value : Nat) (target : BasicBlockId) : SwitchTarget

def Miri.MIR.instReprSwitchTarget.repr : SwitchTarget → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprSwitchTarget : Repr SwitchTarget

Equations

• Miri.MIR.instReprSwitchTarget = { reprPrec := Miri.MIR.instReprSwitchTarget.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqSwitchTarget : DecidableEq SwitchTarget

Equations

• Miri.MIR.instDecidableEqSwitchTarget = Miri.MIR.instDecidableEqSwitchTarget.decEq

def Miri.MIR.instDecidableEqSwitchTarget.decEq (x✝ x✝¹ : SwitchTarget) : Decidable (x✝ = x✝¹)

Equations

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

structure Miri.MIR.SwitchTargets : Type

• cases : Array SwitchTarget
• otherwise : BasicBlockId

@[instance_reducible]

instance Miri.MIR.instReprSwitchTargets : Repr SwitchTargets

Equations

• Miri.MIR.instReprSwitchTargets = { reprPrec := Miri.MIR.instReprSwitchTargets.repr }

def Miri.MIR.instReprSwitchTargets.repr : SwitchTargets → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqSwitchTargets : DecidableEq SwitchTargets

Equations

• Miri.MIR.instDecidableEqSwitchTargets = Miri.MIR.instDecidableEqSwitchTargets.decEq

def Miri.MIR.instDecidableEqSwitchTargets.decEq (x✝ x✝¹ : SwitchTargets) : Decidable (x✝ = x✝¹)

Equations

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

structure Miri.MIR.SpannedOperand : Type

• span : SpanRef
• operand : Operand

def Miri.MIR.instReprSpannedOperand.repr : SpannedOperand → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprSpannedOperand : Repr SpannedOperand

Equations

• Miri.MIR.instReprSpannedOperand = { reprPrec := Miri.MIR.instReprSpannedOperand.repr }

def Miri.MIR.instDecidableEqSpannedOperand.decEq (x✝ x✝¹ : SpannedOperand) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqSpannedOperand.decEq { span := a, operand := a_1 } { span := b, operand := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqSpannedOperand : DecidableEq SpannedOperand

Equations

• Miri.MIR.instDecidableEqSpannedOperand = Miri.MIR.instDecidableEqSpannedOperand.decEq

structure Miri.MIR.InlineAsmOptions : Type

• pure : Bool
• nomem : Bool
• readonly : Bool
• preservesFlags : Bool
• noReturn : Bool
• noStack : Bool
• attSyntax : Bool
• raw : Bool
• mayUnwind : Bool

def Miri.MIR.instReprInlineAsmOptions.repr : InlineAsmOptions → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprInlineAsmOptions : Repr InlineAsmOptions

Equations

• Miri.MIR.instReprInlineAsmOptions = { reprPrec := Miri.MIR.instReprInlineAsmOptions.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqInlineAsmOptions : DecidableEq InlineAsmOptions

Equations

• Miri.MIR.instDecidableEqInlineAsmOptions = Miri.MIR.instDecidableEqInlineAsmOptions.decEq

def Miri.MIR.instDecidableEqInlineAsmOptions.decEq (x✝ x✝¹ : InlineAsmOptions) : Decidable (x✝ = x✝¹)

Equations

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

inductive Miri.MIR.InlineAsmTemplatePiece : Type

• String (text : _root_.String) : InlineAsmTemplatePiece
• Placeholder (operandIndex : Nat) (modifier : Option Char) (span : SpanRef) : InlineAsmTemplatePiece

def Miri.MIR.instReprInlineAsmTemplatePiece.repr : InlineAsmTemplatePiece → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprInlineAsmTemplatePiece : Repr InlineAsmTemplatePiece

Equations

• Miri.MIR.instReprInlineAsmTemplatePiece = { reprPrec := Miri.MIR.instReprInlineAsmTemplatePiece.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqInlineAsmTemplatePiece : DecidableEq InlineAsmTemplatePiece

Equations

• Miri.MIR.instDecidableEqInlineAsmTemplatePiece = Miri.MIR.instDecidableEqInlineAsmTemplatePiece.decEq

def Miri.MIR.instDecidableEqInlineAsmTemplatePiece.decEq (x✝ x✝¹ : InlineAsmTemplatePiece) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqInlineAsmTemplatePiece.decEq (Miri.MIR.InlineAsmTemplatePiece.String a) (Miri.MIR.InlineAsmTemplatePiece.String b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmTemplatePiece.decEq (Miri.MIR.InlineAsmTemplatePiece.String text) (Miri.MIR.InlineAsmTemplatePiece.Placeholder operandIndex modifier span) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmTemplatePiece.decEq (Miri.MIR.InlineAsmTemplatePiece.Placeholder operandIndex modifier span) (Miri.MIR.InlineAsmTemplatePiece.String text) = isFalse ⋯

The pinned compiler resolves a register to a target-specific enum before constructing MIR. We preserve both the target architecture and the resolved register/class spelling. This is a typed serialization view, not an inline assembly evaluator; the importer must block executable readiness until the machine supports that target/register operation.

inductive Miri.MIR.InlineAsmArch : Type

• X86 : InlineAsmArch
• X86_64 : InlineAsmArch
• Arm : InlineAsmArch
• Arm64EC : InlineAsmArch
• AArch64 : InlineAsmArch
• Amdgpu : InlineAsmArch
• RiscV32 : InlineAsmArch
• RiscV64 : InlineAsmArch
• Nvptx64 : InlineAsmArch
• PowerPC : InlineAsmArch
• PowerPC64 : InlineAsmArch
• Hexagon : InlineAsmArch
• LoongArch32 : InlineAsmArch
• LoongArch64 : InlineAsmArch
• Mips : InlineAsmArch
• Mips64 : InlineAsmArch
• Xtensa : InlineAsmArch
• S390x : InlineAsmArch
• Sparc : InlineAsmArch
• Sparc64 : InlineAsmArch
• SpirV : InlineAsmArch
• Wasm32 : InlineAsmArch
• Wasm64 : InlineAsmArch
• Bpf : InlineAsmArch
• Avr : InlineAsmArch
• Msp430 : InlineAsmArch
• M68k : InlineAsmArch
• CSky : InlineAsmArch

@[instance_reducible]

instance Miri.MIR.instReprInlineAsmArch : Repr InlineAsmArch

Equations

• Miri.MIR.instReprInlineAsmArch = { reprPrec := Miri.MIR.instReprInlineAsmArch.repr }

def Miri.MIR.instReprInlineAsmArch.repr : InlineAsmArch → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqInlineAsmArch : DecidableEq InlineAsmArch

Equations

• Miri.MIR.instDecidableEqInlineAsmArch x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Miri.MIR.InlineAsmRegOrRegClass : Type

• Reg (arch : InlineAsmArch) (resolvedRegister : String) : InlineAsmRegOrRegClass
• RegClass (arch : InlineAsmArch) (resolvedClass : String) : InlineAsmRegOrRegClass

def Miri.MIR.instReprInlineAsmRegOrRegClass.repr : InlineAsmRegOrRegClass → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprInlineAsmRegOrRegClass : Repr InlineAsmRegOrRegClass

Equations

• Miri.MIR.instReprInlineAsmRegOrRegClass = { reprPrec := Miri.MIR.instReprInlineAsmRegOrRegClass.repr }

@[instance_reducible]

instance Miri.MIR.instDecidableEqInlineAsmRegOrRegClass : DecidableEq InlineAsmRegOrRegClass

Equations

• Miri.MIR.instDecidableEqInlineAsmRegOrRegClass = Miri.MIR.instDecidableEqInlineAsmRegOrRegClass.decEq

def Miri.MIR.instDecidableEqInlineAsmRegOrRegClass.decEq (x✝ x✝¹ : InlineAsmRegOrRegClass) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqInlineAsmRegOrRegClass.decEq (Miri.MIR.InlineAsmRegOrRegClass.Reg arch resolvedRegister) (Miri.MIR.InlineAsmRegOrRegClass.RegClass arch_1 resolvedClass) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmRegOrRegClass.decEq (Miri.MIR.InlineAsmRegOrRegClass.RegClass arch resolvedClass) (Miri.MIR.InlineAsmRegOrRegClass.Reg arch_1 resolvedRegister) = isFalse ⋯

inductive Miri.MIR.InlineAsmOperand : Type

• In (register : InlineAsmRegOrRegClass) (value : Operand) : InlineAsmOperand
• Out (register : InlineAsmRegOrRegClass) (late : Bool) (place : Option Place) : InlineAsmOperand
• InOut (register : InlineAsmRegOrRegClass) (late : Bool) (input : Operand) (output : Option Place) : InlineAsmOperand
• Const (value : ConstOperand) : InlineAsmOperand
• SymFn (value : ConstOperand) : InlineAsmOperand
• SymStatic (definition : DefId) : InlineAsmOperand
• Label (targetIndex : Nat) : InlineAsmOperand

@[instance_reducible]

instance Miri.MIR.instReprInlineAsmOperand : Repr InlineAsmOperand

Equations

• Miri.MIR.instReprInlineAsmOperand = { reprPrec := Miri.MIR.instReprInlineAsmOperand.repr }

def Miri.MIR.instReprInlineAsmOperand.repr : InlineAsmOperand → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqInlineAsmOperand : DecidableEq InlineAsmOperand

Equations

• Miri.MIR.instDecidableEqInlineAsmOperand = Miri.MIR.instDecidableEqInlineAsmOperand.decEq

def Miri.MIR.instDecidableEqInlineAsmOperand.decEq (x✝ x✝¹ : InlineAsmOperand) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.In register value) (Miri.MIR.InlineAsmOperand.Out register_1 late place) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.In register value) (Miri.MIR.InlineAsmOperand.InOut register_1 late input output) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.In register value) (Miri.MIR.InlineAsmOperand.Const value_1) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.In register value) (Miri.MIR.InlineAsmOperand.SymFn value_1) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.In register value) (Miri.MIR.InlineAsmOperand.SymStatic definition) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.In register value) (Miri.MIR.InlineAsmOperand.Label targetIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Out register late place) (Miri.MIR.InlineAsmOperand.In register_1 value) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Out register late place) (Miri.MIR.InlineAsmOperand.InOut register_1 late_1 input output) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Out register late place) (Miri.MIR.InlineAsmOperand.Const value) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Out register late place) (Miri.MIR.InlineAsmOperand.SymFn value) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Out register late place) (Miri.MIR.InlineAsmOperand.SymStatic definition) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Out register late place) (Miri.MIR.InlineAsmOperand.Label targetIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.InOut register late input output) (Miri.MIR.InlineAsmOperand.In register_1 value) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.InOut register late input output) (Miri.MIR.InlineAsmOperand.Out register_1 late_1 place) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.InOut register late input output) (Miri.MIR.InlineAsmOperand.Const value) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.InOut register late input output) (Miri.MIR.InlineAsmOperand.SymFn value) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.InOut register late input output) (Miri.MIR.InlineAsmOperand.SymStatic definition) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.InOut register late input output) (Miri.MIR.InlineAsmOperand.Label targetIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Const value) (Miri.MIR.InlineAsmOperand.In register value_1) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Const value) (Miri.MIR.InlineAsmOperand.Out register late place) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Const value) (Miri.MIR.InlineAsmOperand.InOut register late input output) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Const a) (Miri.MIR.InlineAsmOperand.Const b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Const value) (Miri.MIR.InlineAsmOperand.SymFn value_1) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Const value) (Miri.MIR.InlineAsmOperand.SymStatic definition) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Const value) (Miri.MIR.InlineAsmOperand.Label targetIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.SymFn value) (Miri.MIR.InlineAsmOperand.In register value_1) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.SymFn value) (Miri.MIR.InlineAsmOperand.Out register late place) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.SymFn value) (Miri.MIR.InlineAsmOperand.InOut register late input output) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.SymFn value) (Miri.MIR.InlineAsmOperand.Const value_1) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.SymFn a) (Miri.MIR.InlineAsmOperand.SymFn b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.SymFn value) (Miri.MIR.InlineAsmOperand.SymStatic definition) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.SymFn value) (Miri.MIR.InlineAsmOperand.Label targetIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.SymStatic definition) (Miri.MIR.InlineAsmOperand.In register value) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.SymStatic definition) (Miri.MIR.InlineAsmOperand.Out register late place) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.SymStatic definition) (Miri.MIR.InlineAsmOperand.InOut register late input output) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.SymStatic definition) (Miri.MIR.InlineAsmOperand.Const value) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.SymStatic definition) (Miri.MIR.InlineAsmOperand.SymFn value) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.SymStatic a) (Miri.MIR.InlineAsmOperand.SymStatic b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.SymStatic definition) (Miri.MIR.InlineAsmOperand.Label targetIndex) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Label targetIndex) (Miri.MIR.InlineAsmOperand.In register value) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Label targetIndex) (Miri.MIR.InlineAsmOperand.Out register late place) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Label targetIndex) (Miri.MIR.InlineAsmOperand.InOut register late input output) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Label targetIndex) (Miri.MIR.InlineAsmOperand.Const value) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Label targetIndex) (Miri.MIR.InlineAsmOperand.SymFn value) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Label targetIndex) (Miri.MIR.InlineAsmOperand.SymStatic definition) = isFalse ⋯
• Miri.MIR.instDecidableEqInlineAsmOperand.decEq (Miri.MIR.InlineAsmOperand.Label a) (Miri.MIR.InlineAsmOperand.Label b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

structure Miri.MIR.InlineAsmTerminator : Type

• asmMacro : InlineAsmMacro
• template : Array InlineAsmTemplatePiece
• operands : Array InlineAsmOperand
• options : InlineAsmOptions
• lineSpans : Array SpanRef
• targets : Array BasicBlockId
• unwind : UnwindAction

@[instance_reducible]

instance Miri.MIR.instReprInlineAsmTerminator : Repr InlineAsmTerminator

Equations

• Miri.MIR.instReprInlineAsmTerminator = { reprPrec := Miri.MIR.instReprInlineAsmTerminator.repr }

def Miri.MIR.instReprInlineAsmTerminator.repr : InlineAsmTerminator → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqInlineAsmTerminator : DecidableEq InlineAsmTerminator

Equations

• Miri.MIR.instDecidableEqInlineAsmTerminator = Miri.MIR.instDecidableEqInlineAsmTerminator.decEq

def Miri.MIR.instDecidableEqInlineAsmTerminator.decEq (x✝ x✝¹ : InlineAsmTerminator) : Decidable (x✝ = x✝¹)

Equations

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

inductive Miri.MIR.AssertKind : Type

• BoundsCheck (length index : Operand) : AssertKind
• Overflow (operator : BinOp) (left right : Operand) : AssertKind
• OverflowNeg (operand : Operand) : AssertKind
• DivisionByZero (operand : Operand) : AssertKind
• RemainderByZero (operand : Operand) : AssertKind
• ResumedAfterReturn (coroutine : CoroutineKind) : AssertKind
• ResumedAfterPanic (coroutine : CoroutineKind) : AssertKind
• ResumedAfterDrop (coroutine : CoroutineKind) : AssertKind
• MisalignedPointerDereference (required found : Operand) : AssertKind
• NullPointerDereference : AssertKind
• NullReferenceConstructed : AssertKind
• InvalidEnumConstruction (operand : Operand) : AssertKind

def Miri.MIR.instReprAssertKind.repr : AssertKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprAssertKind : Repr AssertKind

Equations

• Miri.MIR.instReprAssertKind = { reprPrec := Miri.MIR.instReprAssertKind.repr }

def Miri.MIR.instDecidableEqAssertKind.decEq (x✝ x✝¹ : AssertKind) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqAssertKind : DecidableEq AssertKind

Equations

• Miri.MIR.instDecidableEqAssertKind = Miri.MIR.instDecidableEqAssertKind.decEq

inductive Miri.MIR.TerminatorKind : Type

• Goto (target : BasicBlockId) (loopHints : Array LoopHintAttr) : TerminatorKind
• SwitchInt (discriminant : Operand) (targets : SwitchTargets) : TerminatorKind
• UnwindResume : TerminatorKind
• UnwindTerminate (reason : UnwindTerminateReason) : TerminatorKind
• Return : TerminatorKind
• Unreachable : TerminatorKind
• Drop (place : Place) (target : BasicBlockId) (unwind : UnwindAction) (replace : Bool) (asyncDrop : Option BasicBlockId) : TerminatorKind
• Call (function : Operand) (arguments : Array SpannedOperand) (destination : Place) (target : Option BasicBlockId) (unwind : UnwindAction) (source : CallSource) (functionSpan : SpanRef) : TerminatorKind
• TailCall (function : Operand) (arguments : Array SpannedOperand) (functionSpan : SpanRef) : TerminatorKind
• Assert (condition : Operand) (expected : Bool) (message : AssertKind) (target : BasicBlockId) (unwind : UnwindAction) : TerminatorKind
• Yield (value : Operand) (resume : BasicBlockId) (resumeArgument : Place) (drop : Option BasicBlockId) : TerminatorKind
• CoroutineDrop : TerminatorKind
• FalseEdge (realTarget imaginaryTarget : BasicBlockId) : TerminatorKind
• FalseUnwind (realTarget : BasicBlockId) (unwind : UnwindAction) : TerminatorKind
• InlineAsm (asm : InlineAsmTerminator) : TerminatorKind

def Miri.MIR.instReprTerminatorKind.repr : TerminatorKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprTerminatorKind : Repr TerminatorKind

Equations

• Miri.MIR.instReprTerminatorKind = { reprPrec := Miri.MIR.instReprTerminatorKind.repr }

def Miri.MIR.instDecidableEqTerminatorKind.decEq (x✝ x✝¹ : TerminatorKind) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqTerminatorKind : DecidableEq TerminatorKind

Equations

• Miri.MIR.instDecidableEqTerminatorKind = Miri.MIR.instDecidableEqTerminatorKind.decEq

structure Miri.MIR.SourceInfo : Type

• span : SpanRef
• scope : Nat

@[instance_reducible]

instance Miri.MIR.instReprSourceInfo : Repr SourceInfo

Equations

• Miri.MIR.instReprSourceInfo = { reprPrec := Miri.MIR.instReprSourceInfo.repr }

def Miri.MIR.instReprSourceInfo.repr : SourceInfo → Nat → Std.Format

Equations

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

def Miri.MIR.instDecidableEqSourceInfo.decEq (x✝ x✝¹ : SourceInfo) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqSourceInfo.decEq { span := a, scope := a_1 } { span := b, scope := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqSourceInfo : DecidableEq SourceInfo

Equations

• Miri.MIR.instDecidableEqSourceInfo = Miri.MIR.instDecidableEqSourceInfo.decEq

structure Miri.MIR.Statement : Type

• sourceInfo : SourceInfo
• kind : StatementKind

@[instance_reducible]

instance Miri.MIR.instReprStatement : Repr Statement

Equations

• Miri.MIR.instReprStatement = { reprPrec := Miri.MIR.instReprStatement.repr }

def Miri.MIR.instReprStatement.repr : Statement → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqStatement : DecidableEq Statement

Equations

• Miri.MIR.instDecidableEqStatement = Miri.MIR.instDecidableEqStatement.decEq

def Miri.MIR.instDecidableEqStatement.decEq (x✝ x✝¹ : Statement) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqStatement.decEq { sourceInfo := a, kind := a_1 } { sourceInfo := b, kind := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

structure Miri.MIR.Terminator : Type

• sourceInfo : SourceInfo
• kind : TerminatorKind

@[instance_reducible]

instance Miri.MIR.instReprTerminator : Repr Terminator

Equations

• Miri.MIR.instReprTerminator = { reprPrec := Miri.MIR.instReprTerminator.repr }

def Miri.MIR.instReprTerminator.repr : Terminator → Nat → Std.Format

Equations

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

def Miri.MIR.instDecidableEqTerminator.decEq (x✝ x✝¹ : Terminator) : Decidable (x✝ = x✝¹)

Equations

• Miri.MIR.instDecidableEqTerminator.decEq { sourceInfo := a, kind := a_1 } { sourceInfo := b, kind := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.MIR.instDecidableEqTerminator : DecidableEq Terminator

Equations

• Miri.MIR.instDecidableEqTerminator = Miri.MIR.instDecidableEqTerminator.decEq

structure Miri.MIR.BasicBlock : Type

• statements : Array Statement
• terminator : Terminator
• cleanup : Bool

@[instance_reducible]

instance Miri.MIR.instReprBasicBlock : Repr BasicBlock

Equations

• Miri.MIR.instReprBasicBlock = { reprPrec := Miri.MIR.instReprBasicBlock.repr }

def Miri.MIR.instReprBasicBlock.repr : BasicBlock → Nat → Std.Format

Equations

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

def Miri.MIR.instDecidableEqBasicBlock.decEq (x✝ x✝¹ : BasicBlock) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqBasicBlock : DecidableEq BasicBlock

Equations

• Miri.MIR.instDecidableEqBasicBlock = Miri.MIR.instDecidableEqBasicBlock.decEq

structure Miri.MIR.Body : Type

• phase : MirPhase
• argumentCount : Nat
• spreadArgument : Option LocalId
• locals : Array TyId
• basicBlocks : Array BasicBlock

@[instance_reducible]

instance Miri.MIR.instReprBody : Repr Body

Equations

• Miri.MIR.instReprBody = { reprPrec := Miri.MIR.instReprBody.repr }

def Miri.MIR.instReprBody.repr : Body → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.MIR.instDecidableEqBody : DecidableEq Body

Equations

• Miri.MIR.instDecidableEqBody = Miri.MIR.instDecidableEqBody.decEq

def Miri.MIR.instDecidableEqBody.decEq (x✝ x✝¹ : Body) : Decidable (x✝ = x✝¹)

Equations

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