(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module ops.
  Module arith.
    (* Trait *)
    (* Empty module 'Add' *)
    
    Module Impl_core_ops_arith_Add_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "usize".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_usize.
    
    Module Impl_core_ops_arith_Add_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u8".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_u8.
    
    Module Impl_core_ops_arith_Add_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u16".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_u16.
    
    Module Impl_core_ops_arith_Add_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u32".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_u32.
    
    Module Impl_core_ops_arith_Add_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u64".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_u64.
    
    Module Impl_core_ops_arith_Add_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u128".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_u128.
    
    Module Impl_core_ops_arith_Add_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "isize".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_isize.
    
    Module Impl_core_ops_arith_Add_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i8".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_i8.
    
    Module Impl_core_ops_arith_Add_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i16".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_i16.
    
    Module Impl_core_ops_arith_Add_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i32".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_i32.
    
    Module Impl_core_ops_arith_Add_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i64".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_i64.
    
    Module Impl_core_ops_arith_Add_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i128".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_i128.
    
    Module Impl_core_ops_arith_Add_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f16".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_f16.
    
    Module Impl_core_ops_arith_Add_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f32".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_f32.
    
    Module Impl_core_ops_arith_Add_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f64".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_f64.
    
    Module Impl_core_ops_arith_Add_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f128".
      
      (*             fn add(self, other: $t) -> $t { self + other } *)
      Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.add (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Add"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
    End Impl_core_ops_arith_Add_for_f128.
    
    (* Trait *)
    (* Empty module 'Sub' *)
    
    Module Impl_core_ops_arith_Sub_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "usize".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_usize.
    
    Module Impl_core_ops_arith_Sub_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u8".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_u8.
    
    Module Impl_core_ops_arith_Sub_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u16".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_u16.
    
    Module Impl_core_ops_arith_Sub_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u32".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_u32.
    
    Module Impl_core_ops_arith_Sub_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u64".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_u64.
    
    Module Impl_core_ops_arith_Sub_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u128".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_u128.
    
    Module Impl_core_ops_arith_Sub_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "isize".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_isize.
    
    Module Impl_core_ops_arith_Sub_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i8".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_i8.
    
    Module Impl_core_ops_arith_Sub_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i16".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_i16.
    
    Module Impl_core_ops_arith_Sub_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i32".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_i32.
    
    Module Impl_core_ops_arith_Sub_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i64".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_i64.
    
    Module Impl_core_ops_arith_Sub_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i128".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_i128.
    
    Module Impl_core_ops_arith_Sub_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f16".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_f16.
    
    Module Impl_core_ops_arith_Sub_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f32".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_f32.
    
    Module Impl_core_ops_arith_Sub_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f64".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_f64.
    
    Module Impl_core_ops_arith_Sub_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f128".
      
      (*             fn sub(self, other: $t) -> $t { self - other } *)
      Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.sub (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Sub"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
    End Impl_core_ops_arith_Sub_for_f128.
    
    (* Trait *)
    (* Empty module 'Mul' *)
    
    Module Impl_core_ops_arith_Mul_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "usize".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_usize.
    
    Module Impl_core_ops_arith_Mul_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u8".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_u8.
    
    Module Impl_core_ops_arith_Mul_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u16".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_u16.
    
    Module Impl_core_ops_arith_Mul_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u32".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_u32.
    
    Module Impl_core_ops_arith_Mul_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u64".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_u64.
    
    Module Impl_core_ops_arith_Mul_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u128".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_u128.
    
    Module Impl_core_ops_arith_Mul_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "isize".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_isize.
    
    Module Impl_core_ops_arith_Mul_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i8".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_i8.
    
    Module Impl_core_ops_arith_Mul_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i16".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_i16.
    
    Module Impl_core_ops_arith_Mul_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i32".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_i32.
    
    Module Impl_core_ops_arith_Mul_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i64".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_i64.
    
    Module Impl_core_ops_arith_Mul_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i128".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_i128.
    
    Module Impl_core_ops_arith_Mul_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f16".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_f16.
    
    Module Impl_core_ops_arith_Mul_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f32".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_f32.
    
    Module Impl_core_ops_arith_Mul_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f64".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_f64.
    
    Module Impl_core_ops_arith_Mul_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f128".
      
      (*             fn mul(self, other: $t) -> $t { self * other } *)
      Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.mul (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Mul"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
    End Impl_core_ops_arith_Mul_for_f128.
    
    (* Trait *)
    (* Empty module 'Div' *)
    
    Module Impl_core_ops_arith_Div_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "usize".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_usize.
    
    Module Impl_core_ops_arith_Div_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u8".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_u8.
    
    Module Impl_core_ops_arith_Div_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u16".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_u16.
    
    Module Impl_core_ops_arith_Div_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u32".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_u32.
    
    Module Impl_core_ops_arith_Div_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u64".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_u64.
    
    Module Impl_core_ops_arith_Div_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u128".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_u128.
    
    Module Impl_core_ops_arith_Div_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "isize".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_isize.
    
    Module Impl_core_ops_arith_Div_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i8".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_i8.
    
    Module Impl_core_ops_arith_Div_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i16".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_i16.
    
    Module Impl_core_ops_arith_Div_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i32".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_i32.
    
    Module Impl_core_ops_arith_Div_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i64".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_i64.
    
    Module Impl_core_ops_arith_Div_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i128".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_i128.
    
    Module Impl_core_ops_arith_Div_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f16".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_f16.
    
    Module Impl_core_ops_arith_Div_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f32".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_f32.
    
    Module Impl_core_ops_arith_Div_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f64".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_f64.
    
    Module Impl_core_ops_arith_Div_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f128".
      
      (*             fn div(self, other: $t) -> $t { self / other } *)
      Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.div (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Div"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
    End Impl_core_ops_arith_Div_for_f128.
    
    (* Trait *)
    (* Empty module 'Rem' *)
    
    Module Impl_core_ops_arith_Rem_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "usize".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_usize.
    
    Module Impl_core_ops_arith_Rem_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u8".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_u8.
    
    Module Impl_core_ops_arith_Rem_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u16".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_u16.
    
    Module Impl_core_ops_arith_Rem_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u32".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_u32.
    
    Module Impl_core_ops_arith_Rem_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u64".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_u64.
    
    Module Impl_core_ops_arith_Rem_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "u128".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_u128.
    
    Module Impl_core_ops_arith_Rem_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "isize".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_isize.
    
    Module Impl_core_ops_arith_Rem_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i8".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_i8.
    
    Module Impl_core_ops_arith_Rem_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i16".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_i16.
    
    Module Impl_core_ops_arith_Rem_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i32".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_i32.
    
    Module Impl_core_ops_arith_Rem_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i64".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_i64.
    
    Module Impl_core_ops_arith_Rem_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i128".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_i128.
    
    Module Impl_core_ops_arith_Rem_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f16".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_f16.
    
    Module Impl_core_ops_arith_Rem_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f32".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_f32.
    
    Module Impl_core_ops_arith_Rem_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f64".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_f64.
    
    Module Impl_core_ops_arith_Rem_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f128".
      
      (*             fn rem(self, other: $t) -> $t { self % other } *)
      Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.Wrap.rem (| M.read (| self |), M.read (| other |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Rem"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
    End Impl_core_ops_arith_Rem_for_f128.
    
    (* Trait *)
    (* Empty module 'Neg' *)
    
    Module Impl_core_ops_arith_Neg_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "isize".
      
      (*             fn neg(self) -> $t { -self } *)
      Definition neg (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            UnOp.neg (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Neg"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("neg", InstanceField.Method neg) ].
    End Impl_core_ops_arith_Neg_for_isize.
    
    Module Impl_core_ops_arith_Neg_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i8".
      
      (*             fn neg(self) -> $t { -self } *)
      Definition neg (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            UnOp.neg (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Neg"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("neg", InstanceField.Method neg) ].
    End Impl_core_ops_arith_Neg_for_i8.
    
    Module Impl_core_ops_arith_Neg_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i16".
      
      (*             fn neg(self) -> $t { -self } *)
      Definition neg (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            UnOp.neg (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Neg"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("neg", InstanceField.Method neg) ].
    End Impl_core_ops_arith_Neg_for_i16.
    
    Module Impl_core_ops_arith_Neg_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i32".
      
      (*             fn neg(self) -> $t { -self } *)
      Definition neg (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            UnOp.neg (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Neg"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("neg", InstanceField.Method neg) ].
    End Impl_core_ops_arith_Neg_for_i32.
    
    Module Impl_core_ops_arith_Neg_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i64".
      
      (*             fn neg(self) -> $t { -self } *)
      Definition neg (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            UnOp.neg (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Neg"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("neg", InstanceField.Method neg) ].
    End Impl_core_ops_arith_Neg_for_i64.
    
    Module Impl_core_ops_arith_Neg_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "i128".
      
      (*             fn neg(self) -> $t { -self } *)
      Definition neg (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            UnOp.neg (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Neg"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("neg", InstanceField.Method neg) ].
    End Impl_core_ops_arith_Neg_for_i128.
    
    Module Impl_core_ops_arith_Neg_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f16".
      
      (*             fn neg(self) -> $t { -self } *)
      Definition neg (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            UnOp.neg (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Neg"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("neg", InstanceField.Method neg) ].
    End Impl_core_ops_arith_Neg_for_f16.
    
    Module Impl_core_ops_arith_Neg_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f32".
      
      (*             fn neg(self) -> $t { -self } *)
      Definition neg (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            UnOp.neg (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Neg"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("neg", InstanceField.Method neg) ].
    End Impl_core_ops_arith_Neg_for_f32.
    
    Module Impl_core_ops_arith_Neg_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f64".
      
      (*             fn neg(self) -> $t { -self } *)
      Definition neg (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            UnOp.neg (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Neg"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("neg", InstanceField.Method neg) ].
    End Impl_core_ops_arith_Neg_for_f64.
    
    Module Impl_core_ops_arith_Neg_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*             type Output = $t; *)
      Definition _Output : Ty.t := Ty.path "f128".
      
      (*             fn neg(self) -> $t { -self } *)
      Definition neg (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            UnOp.neg (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::Neg"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Output", InstanceField.Ty _Output); ("neg", InstanceField.Method neg) ].
    End Impl_core_ops_arith_Neg_for_f128.
    
    (* Trait *)
    (* Empty module 'AddAssign' *)
    
    Module Impl_core_ops_arith_AddAssign_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_usize.
    
    Module Impl_core_ops_arith_AddAssign_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_u8.
    
    Module Impl_core_ops_arith_AddAssign_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_u16.
    
    Module Impl_core_ops_arith_AddAssign_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_u32.
    
    Module Impl_core_ops_arith_AddAssign_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_u64.
    
    Module Impl_core_ops_arith_AddAssign_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_u128.
    
    Module Impl_core_ops_arith_AddAssign_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_isize.
    
    Module Impl_core_ops_arith_AddAssign_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_i8.
    
    Module Impl_core_ops_arith_AddAssign_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_i16.
    
    Module Impl_core_ops_arith_AddAssign_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_i32.
    
    Module Impl_core_ops_arith_AddAssign_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_i64.
    
    Module Impl_core_ops_arith_AddAssign_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_i128.
    
    Module Impl_core_ops_arith_AddAssign_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_f16.
    
    Module Impl_core_ops_arith_AddAssign_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_f32.
    
    Module Impl_core_ops_arith_AddAssign_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_f64.
    
    Module Impl_core_ops_arith_AddAssign_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*             fn add_assign(&mut self, other: $t) { *self += other } *)
      Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.add (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::AddAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
    End Impl_core_ops_arith_AddAssign_for_f128.
    
    (* Trait *)
    (* Empty module 'SubAssign' *)
    
    Module Impl_core_ops_arith_SubAssign_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_usize.
    
    Module Impl_core_ops_arith_SubAssign_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_u8.
    
    Module Impl_core_ops_arith_SubAssign_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_u16.
    
    Module Impl_core_ops_arith_SubAssign_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_u32.
    
    Module Impl_core_ops_arith_SubAssign_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_u64.
    
    Module Impl_core_ops_arith_SubAssign_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_u128.
    
    Module Impl_core_ops_arith_SubAssign_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_isize.
    
    Module Impl_core_ops_arith_SubAssign_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_i8.
    
    Module Impl_core_ops_arith_SubAssign_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_i16.
    
    Module Impl_core_ops_arith_SubAssign_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_i32.
    
    Module Impl_core_ops_arith_SubAssign_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_i64.
    
    Module Impl_core_ops_arith_SubAssign_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_i128.
    
    Module Impl_core_ops_arith_SubAssign_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_f16.
    
    Module Impl_core_ops_arith_SubAssign_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_f32.
    
    Module Impl_core_ops_arith_SubAssign_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_f64.
    
    Module Impl_core_ops_arith_SubAssign_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*             fn sub_assign(&mut self, other: $t) { *self -= other } *)
      Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::SubAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
    End Impl_core_ops_arith_SubAssign_for_f128.
    
    (* Trait *)
    (* Empty module 'MulAssign' *)
    
    Module Impl_core_ops_arith_MulAssign_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_usize.
    
    Module Impl_core_ops_arith_MulAssign_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_u8.
    
    Module Impl_core_ops_arith_MulAssign_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_u16.
    
    Module Impl_core_ops_arith_MulAssign_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_u32.
    
    Module Impl_core_ops_arith_MulAssign_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_u64.
    
    Module Impl_core_ops_arith_MulAssign_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_u128.
    
    Module Impl_core_ops_arith_MulAssign_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_isize.
    
    Module Impl_core_ops_arith_MulAssign_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_i8.
    
    Module Impl_core_ops_arith_MulAssign_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_i16.
    
    Module Impl_core_ops_arith_MulAssign_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_i32.
    
    Module Impl_core_ops_arith_MulAssign_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_i64.
    
    Module Impl_core_ops_arith_MulAssign_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_i128.
    
    Module Impl_core_ops_arith_MulAssign_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_f16.
    
    Module Impl_core_ops_arith_MulAssign_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_f32.
    
    Module Impl_core_ops_arith_MulAssign_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_f64.
    
    Module Impl_core_ops_arith_MulAssign_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*             fn mul_assign(&mut self, other: $t) { *self *= other } *)
      Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.mul (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::MulAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
    End Impl_core_ops_arith_MulAssign_for_f128.
    
    (* Trait *)
    (* Empty module 'DivAssign' *)
    
    Module Impl_core_ops_arith_DivAssign_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_usize.
    
    Module Impl_core_ops_arith_DivAssign_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_u8.
    
    Module Impl_core_ops_arith_DivAssign_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_u16.
    
    Module Impl_core_ops_arith_DivAssign_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_u32.
    
    Module Impl_core_ops_arith_DivAssign_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_u64.
    
    Module Impl_core_ops_arith_DivAssign_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_u128.
    
    Module Impl_core_ops_arith_DivAssign_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_isize.
    
    Module Impl_core_ops_arith_DivAssign_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_i8.
    
    Module Impl_core_ops_arith_DivAssign_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_i16.
    
    Module Impl_core_ops_arith_DivAssign_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_i32.
    
    Module Impl_core_ops_arith_DivAssign_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_i64.
    
    Module Impl_core_ops_arith_DivAssign_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_i128.
    
    Module Impl_core_ops_arith_DivAssign_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_f16.
    
    Module Impl_core_ops_arith_DivAssign_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_f32.
    
    Module Impl_core_ops_arith_DivAssign_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_f64.
    
    Module Impl_core_ops_arith_DivAssign_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*             fn div_assign(&mut self, other: $t) { *self /= other } *)
      Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.div (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::DivAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
    End Impl_core_ops_arith_DivAssign_for_f128.
    
    (* Trait *)
    (* Empty module 'RemAssign' *)
    
    Module Impl_core_ops_arith_RemAssign_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_usize.
    
    Module Impl_core_ops_arith_RemAssign_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_u8.
    
    Module Impl_core_ops_arith_RemAssign_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_u16.
    
    Module Impl_core_ops_arith_RemAssign_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_u32.
    
    Module Impl_core_ops_arith_RemAssign_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_u64.
    
    Module Impl_core_ops_arith_RemAssign_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_u128.
    
    Module Impl_core_ops_arith_RemAssign_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_isize.
    
    Module Impl_core_ops_arith_RemAssign_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_i8.
    
    Module Impl_core_ops_arith_RemAssign_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_i16.
    
    Module Impl_core_ops_arith_RemAssign_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_i32.
    
    Module Impl_core_ops_arith_RemAssign_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_i64.
    
    Module Impl_core_ops_arith_RemAssign_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_i128.
    
    Module Impl_core_ops_arith_RemAssign_for_f16.
      Definition Self : Ty.t := Ty.path "f16".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_f16.
    
    Module Impl_core_ops_arith_RemAssign_for_f32.
      Definition Self : Ty.t := Ty.path "f32".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_f32.
    
    Module Impl_core_ops_arith_RemAssign_for_f64.
      Definition Self : Ty.t := Ty.path "f64".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_f64.
    
    Module Impl_core_ops_arith_RemAssign_for_f128.
      Definition Self : Ty.t := Ty.path "f128".
      
      (*             fn rem_assign(&mut self, other: $t) { *self %= other } *)
      Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let β := M.read (| self |) in
              M.write (| β, BinOp.Wrap.rem (| M.read (| β |), M.read (| other |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::arith::RemAssign"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
    End Impl_core_ops_arith_RemAssign_for_f128.
  End arith.
End ops.
