Operator tags of the pinned rustc_middle::mir::syntax definitions.

inductive Miri.MIR.IntegerKind : Type

• i8 : IntegerKind
• i16 : IntegerKind
• i32 : IntegerKind
• i64 : IntegerKind
• i128 : IntegerKind
• isize : IntegerKind
• u8 : IntegerKind
• u16 : IntegerKind
• u32 : IntegerKind
• u64 : IntegerKind
• u128 : IntegerKind
• usize : IntegerKind

@[instance_reducible]

instance Miri.MIR.instDecidableEqIntegerKind : DecidableEq IntegerKind

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprIntegerKind : Repr IntegerKind

Equations

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

def Miri.MIR.instReprIntegerKind.repr : IntegerKind → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instReprIntegerKind.repr Miri.MIR.IntegerKind.i8 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.IntegerKind.i8")).group prec✝
• Miri.MIR.instReprIntegerKind.repr Miri.MIR.IntegerKind.i16 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.IntegerKind.i16")).group prec✝
• Miri.MIR.instReprIntegerKind.repr Miri.MIR.IntegerKind.i32 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.IntegerKind.i32")).group prec✝
• Miri.MIR.instReprIntegerKind.repr Miri.MIR.IntegerKind.i64 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.IntegerKind.i64")).group prec✝
• Miri.MIR.instReprIntegerKind.repr Miri.MIR.IntegerKind.i128 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.IntegerKind.i128")).group prec✝
• Miri.MIR.instReprIntegerKind.repr Miri.MIR.IntegerKind.u8 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.IntegerKind.u8")).group prec✝
• Miri.MIR.instReprIntegerKind.repr Miri.MIR.IntegerKind.u16 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.IntegerKind.u16")).group prec✝
• Miri.MIR.instReprIntegerKind.repr Miri.MIR.IntegerKind.u32 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.IntegerKind.u32")).group prec✝
• Miri.MIR.instReprIntegerKind.repr Miri.MIR.IntegerKind.u64 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.IntegerKind.u64")).group prec✝
• Miri.MIR.instReprIntegerKind.repr Miri.MIR.IntegerKind.u128 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.IntegerKind.u128")).group prec✝

def Miri.MIR.IntegerKind.signed : IntegerKind → Bool

Equations

• Miri.MIR.IntegerKind.i8.signed = true
• Miri.MIR.IntegerKind.i16.signed = true
• Miri.MIR.IntegerKind.i32.signed = true
• Miri.MIR.IntegerKind.i64.signed = true
• Miri.MIR.IntegerKind.i128.signed = true
• Miri.MIR.IntegerKind.isize.signed = true
• x✝.signed = false

inductive Miri.MIR.BinOp : Type

• Add : BinOp
• AddUnchecked : BinOp
• AddWithOverflow : BinOp
• Sub : BinOp
• SubUnchecked : BinOp
• SubWithOverflow : BinOp
• Mul : BinOp
• MulUnchecked : BinOp
• MulWithOverflow : BinOp
• Div : BinOp
• Rem : BinOp
• BitXor : BinOp
• BitAnd : BinOp
• BitOr : BinOp
• Shl : BinOp
• ShlUnchecked : BinOp
• Shr : BinOp
• ShrUnchecked : BinOp
• Eq : BinOp
• Lt : BinOp
• Le : BinOp
• Ne : BinOp
• Ge : BinOp
• Gt : BinOp
• Cmp : BinOp
• Offset : BinOp

@[instance_reducible]

instance Miri.MIR.instDecidableEqBinOp : DecidableEq BinOp

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprBinOp : Repr BinOp

Equations

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

def Miri.MIR.instReprBinOp.repr : BinOp → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Add prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Add")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.AddUnchecked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.AddUnchecked")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Sub prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Sub")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.SubUnchecked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.SubUnchecked")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Mul prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Mul")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.MulUnchecked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.MulUnchecked")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Div prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Div")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Rem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Rem")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.BitXor prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.BitXor")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.BitAnd prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.BitAnd")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.BitOr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.BitOr")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Shl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Shl")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.ShlUnchecked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.ShlUnchecked")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Shr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Shr")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.ShrUnchecked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.ShrUnchecked")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Eq prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Eq")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Lt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Lt")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Le prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Le")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Ne prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Ne")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Ge prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Ge")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Gt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Gt")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Cmp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Cmp")).group prec✝
• Miri.MIR.instReprBinOp.repr Miri.MIR.BinOp.Offset prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.BinOp.Offset")).group prec✝

inductive Miri.MIR.UnOp : Type

• Not : UnOp
• Neg : UnOp
• PtrMetadata : UnOp

@[instance_reducible]

instance Miri.MIR.instDecidableEqUnOp : DecidableEq UnOp

Equations

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

@[instance_reducible]

instance Miri.MIR.instReprUnOp : Repr UnOp

Equations

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

def Miri.MIR.instReprUnOp.repr : UnOp → Nat → Std.Format

Equations

• Miri.MIR.instReprUnOp.repr Miri.MIR.UnOp.Not prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.UnOp.Not")).group prec✝
• Miri.MIR.instReprUnOp.repr Miri.MIR.UnOp.Neg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.UnOp.Neg")).group prec✝
• Miri.MIR.instReprUnOp.repr Miri.MIR.UnOp.PtrMetadata prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Miri.MIR.UnOp.PtrMetadata")).group prec✝

def Miri.MIR.BinOp.ofString : String → Option BinOp

Equations

• Miri.MIR.BinOp.ofString "Add" = some Miri.MIR.BinOp.Add
• Miri.MIR.BinOp.ofString "AddUnchecked" = some Miri.MIR.BinOp.AddUnchecked
• Miri.MIR.BinOp.ofString "AddWithOverflow" = some Miri.MIR.BinOp.AddWithOverflow
• Miri.MIR.BinOp.ofString "Sub" = some Miri.MIR.BinOp.Sub
• Miri.MIR.BinOp.ofString "SubUnchecked" = some Miri.MIR.BinOp.SubUnchecked
• Miri.MIR.BinOp.ofString "SubWithOverflow" = some Miri.MIR.BinOp.SubWithOverflow
• Miri.MIR.BinOp.ofString "Mul" = some Miri.MIR.BinOp.Mul
• Miri.MIR.BinOp.ofString "MulUnchecked" = some Miri.MIR.BinOp.MulUnchecked
• Miri.MIR.BinOp.ofString "MulWithOverflow" = some Miri.MIR.BinOp.MulWithOverflow
• Miri.MIR.BinOp.ofString "Div" = some Miri.MIR.BinOp.Div
• Miri.MIR.BinOp.ofString "Rem" = some Miri.MIR.BinOp.Rem
• Miri.MIR.BinOp.ofString "BitXor" = some Miri.MIR.BinOp.BitXor
• Miri.MIR.BinOp.ofString "BitAnd" = some Miri.MIR.BinOp.BitAnd
• Miri.MIR.BinOp.ofString "BitOr" = some Miri.MIR.BinOp.BitOr
• Miri.MIR.BinOp.ofString "Shl" = some Miri.MIR.BinOp.Shl
• Miri.MIR.BinOp.ofString "ShlUnchecked" = some Miri.MIR.BinOp.ShlUnchecked
• Miri.MIR.BinOp.ofString "Shr" = some Miri.MIR.BinOp.Shr
• Miri.MIR.BinOp.ofString "ShrUnchecked" = some Miri.MIR.BinOp.ShrUnchecked
• Miri.MIR.BinOp.ofString "Eq" = some Miri.MIR.BinOp.Eq
• Miri.MIR.BinOp.ofString "Lt" = some Miri.MIR.BinOp.Lt
• Miri.MIR.BinOp.ofString "Le" = some Miri.MIR.BinOp.Le
• Miri.MIR.BinOp.ofString "Ne" = some Miri.MIR.BinOp.Ne
• Miri.MIR.BinOp.ofString "Ge" = some Miri.MIR.BinOp.Ge
• Miri.MIR.BinOp.ofString "Gt" = some Miri.MIR.BinOp.Gt
• Miri.MIR.BinOp.ofString "Cmp" = some Miri.MIR.BinOp.Cmp
• Miri.MIR.BinOp.ofString "Offset" = some Miri.MIR.BinOp.Offset
• Miri.MIR.BinOp.ofString x✝ = none

def Miri.MIR.BinOp.isOverflowing : BinOp → Bool

Equations

• Miri.MIR.BinOp.AddWithOverflow.isOverflowing = true
• Miri.MIR.BinOp.SubWithOverflow.isOverflowing = true
• Miri.MIR.BinOp.MulWithOverflow.isOverflowing = true
• x✝.isOverflowing = false

def Miri.MIR.BinOp.isUnchecked : BinOp → Bool

Equations

• Miri.MIR.BinOp.AddUnchecked.isUnchecked = true
• Miri.MIR.BinOp.SubUnchecked.isUnchecked = true
• Miri.MIR.BinOp.MulUnchecked.isUnchecked = true
• Miri.MIR.BinOp.ShlUnchecked.isUnchecked = true
• Miri.MIR.BinOp.ShrUnchecked.isUnchecked = true
• x✝.isUnchecked = false

def Miri.MIR.BinOp.leftHomogeneous : BinOp → Bool

Pinned rustc_const_eval util::binop_left_homogeneous.

Equations

• Miri.MIR.BinOp.Add.leftHomogeneous = true
• Miri.MIR.BinOp.AddUnchecked.leftHomogeneous = true
• Miri.MIR.BinOp.Sub.leftHomogeneous = true
• Miri.MIR.BinOp.SubUnchecked.leftHomogeneous = true
• Miri.MIR.BinOp.Mul.leftHomogeneous = true
• Miri.MIR.BinOp.MulUnchecked.leftHomogeneous = true
• Miri.MIR.BinOp.Div.leftHomogeneous = true
• Miri.MIR.BinOp.Rem.leftHomogeneous = true
• Miri.MIR.BinOp.BitXor.leftHomogeneous = true
• Miri.MIR.BinOp.BitAnd.leftHomogeneous = true
• Miri.MIR.BinOp.BitOr.leftHomogeneous = true
• Miri.MIR.BinOp.Offset.leftHomogeneous = true
• Miri.MIR.BinOp.Shl.leftHomogeneous = true
• Miri.MIR.BinOp.ShlUnchecked.leftHomogeneous = true
• Miri.MIR.BinOp.Shr.leftHomogeneous = true
• Miri.MIR.BinOp.ShrUnchecked.leftHomogeneous = true
• Miri.MIR.BinOp.AddWithOverflow.leftHomogeneous = false
• Miri.MIR.BinOp.SubWithOverflow.leftHomogeneous = false
• Miri.MIR.BinOp.MulWithOverflow.leftHomogeneous = false
• Miri.MIR.BinOp.Eq.leftHomogeneous = false
• Miri.MIR.BinOp.Ne.leftHomogeneous = false
• Miri.MIR.BinOp.Lt.leftHomogeneous = false
• Miri.MIR.BinOp.Le.leftHomogeneous = false
• Miri.MIR.BinOp.Gt.leftHomogeneous = false
• Miri.MIR.BinOp.Ge.leftHomogeneous = false
• Miri.MIR.BinOp.Cmp.leftHomogeneous = false

def Miri.MIR.BinOp.rightHomogeneous : BinOp → Bool

Pinned rustc_const_eval util::binop_right_homogeneous.

Equations

• Miri.MIR.BinOp.Add.rightHomogeneous = true
• Miri.MIR.BinOp.AddUnchecked.rightHomogeneous = true
• Miri.MIR.BinOp.AddWithOverflow.rightHomogeneous = true
• Miri.MIR.BinOp.Sub.rightHomogeneous = true
• Miri.MIR.BinOp.SubUnchecked.rightHomogeneous = true
• Miri.MIR.BinOp.SubWithOverflow.rightHomogeneous = true
• Miri.MIR.BinOp.Mul.rightHomogeneous = true
• Miri.MIR.BinOp.MulUnchecked.rightHomogeneous = true
• Miri.MIR.BinOp.MulWithOverflow.rightHomogeneous = true
• Miri.MIR.BinOp.Div.rightHomogeneous = true
• Miri.MIR.BinOp.Rem.rightHomogeneous = true
• Miri.MIR.BinOp.BitXor.rightHomogeneous = true
• Miri.MIR.BinOp.BitAnd.rightHomogeneous = true
• Miri.MIR.BinOp.BitOr.rightHomogeneous = true
• Miri.MIR.BinOp.Eq.rightHomogeneous = true
• Miri.MIR.BinOp.Ne.rightHomogeneous = true
• Miri.MIR.BinOp.Lt.rightHomogeneous = true
• Miri.MIR.BinOp.Le.rightHomogeneous = true
• Miri.MIR.BinOp.Gt.rightHomogeneous = true
• Miri.MIR.BinOp.Ge.rightHomogeneous = true
• Miri.MIR.BinOp.Cmp.rightHomogeneous = true
• Miri.MIR.BinOp.Offset.rightHomogeneous = false
• Miri.MIR.BinOp.Shl.rightHomogeneous = false
• Miri.MIR.BinOp.ShlUnchecked.rightHomogeneous = false
• Miri.MIR.BinOp.Shr.rightHomogeneous = false
• Miri.MIR.BinOp.ShrUnchecked.rightHomogeneous = false

def Miri.MIR.UnOp.ofString : String → Option UnOp

Equations

• Miri.MIR.UnOp.ofString "Not" = some Miri.MIR.UnOp.Not
• Miri.MIR.UnOp.ofString "Neg" = some Miri.MIR.UnOp.Neg
• Miri.MIR.UnOp.ofString "PtrMetadata" = some Miri.MIR.UnOp.PtrMetadata
• Miri.MIR.UnOp.ofString x✝ = none

def Miri.MIR.UnOp.homogeneous : UnOp → Bool

Pinned rustc_const_eval util::unop_homogeneous.

Equations

• Miri.MIR.UnOp.Not.homogeneous = true
• Miri.MIR.UnOp.Neg.homogeneous = true
• Miri.MIR.UnOp.PtrMetadata.homogeneous = false