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

Module slice.
  Module cmp.
    Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_slice_U_for_slice_T.
      Definition Self (T U : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn eq(&self, other: &[U]) -> bool {
              SlicePartialEq::equal(self, other)
          }
      *)
      Definition eq (T U : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T U in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::cmp::SlicePartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ U ],
                "equal",
                []
              |),
              [ M.read (| self |); M.read (| other |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn ne(&self, other: &[U]) -> bool {
              SlicePartialEq::not_equal(self, other)
          }
      *)
      Definition ne (T U : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T U in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::cmp::SlicePartialEq",
                Ty.apply (Ty.path "slice") [] [ T ],
                [ U ],
                "not_equal",
                []
              |),
              [ M.read (| self |); M.read (| other |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T U : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialEq"
          (Self T U)
          (* Trait polymorphic types *) [ (* Rhs *) Ty.apply (Ty.path "slice") [] [ U ] ]
          (* Instance *)
          [ ("eq", InstanceField.Method (eq T U)); ("ne", InstanceField.Method (ne T U)) ].
    End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_U_slice_U_for_slice_T.
    
    Module Impl_core_cmp_Eq_where_core_cmp_Eq_T_for_slice_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::cmp::Eq"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_cmp_Eq_where_core_cmp_Eq_T_for_slice_T.
    
    Module Impl_core_cmp_Ord_where_core_cmp_Ord_T_for_slice_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn cmp(&self, other: &[T]) -> Ordering {
              SliceOrd::compare(self, other)
          }
      *)
      Definition cmp (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (| "core::slice::cmp::SliceOrd", T, [], "compare", [] |),
              [ M.read (| self |); M.read (| other |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::cmp::Ord"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method (cmp T)) ].
    End Impl_core_cmp_Ord_where_core_cmp_Ord_T_for_slice_T.
    
    Module Impl_core_cmp_PartialOrd_where_core_cmp_PartialOrd_T_for_slice_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ T ].
      
      (*
          fn partial_cmp(&self, other: &[T]) -> Option<Ordering> {
              SlicePartialOrd::partial_compare(self, other)
          }
      *)
      Definition partial_cmp (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::cmp::SlicePartialOrd",
                T,
                [],
                "partial_compare",
                []
              |),
              [ M.read (| self |); M.read (| other |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("partial_cmp", InstanceField.Method (partial_cmp T)) ].
    End Impl_core_cmp_PartialOrd_where_core_cmp_PartialOrd_T_for_slice_T.
    
    (* Trait *)
    Module SlicePartialEq.
      Definition not_equal
          (B Self : Ty.t)
          (ε : 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
            UnOp.not (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::slice::cmp::SlicePartialEq",
                  Self,
                  [ B ],
                  "equal",
                  []
                |),
                [ M.read (| self |); M.read (| other |) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom ProvidedMethod_not_equal :
        forall (B : Ty.t),
        M.IsProvidedMethod "core::slice::cmp::SlicePartialEq" "not_equal" (not_equal B).
    End SlicePartialEq.
    
    Module Impl_core_slice_cmp_SlicePartialEq_where_core_cmp_PartialEq_A_B_B_for_slice_A.
      Definition Self (A B : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ A ].
      
      (*
          default fn equal(&self, other: &[B]) -> bool {
              if self.len() != other.len() {
                  return false;
              }
      
              // Implemented as explicit indexing rather
              // than zipped iterators for performance reasons.
              // See PR https://github.com/rust-lang/rust/pull/116846
              for idx in 0..self.len() {
                  // bound checks are optimized away
                  if self[idx] != other[idx] {
                      return false;
                  }
              }
      
              true
          }
      *)
      Definition equal (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ne (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ A ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |),
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ B ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| other |) ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| Value.Bool false |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.use
                      (M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::collect::IntoIterator",
                              Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                              [],
                              "into_iter",
                              []
                            |),
                            [
                              Value.StructRecord
                                "core::ops::range::Range"
                                [
                                  ("start", Value.Integer IntegerKind.Usize 0);
                                  ("end_",
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ A ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |))
                                ]
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let iter := M.copy (| γ |) in
                              M.loop (|
                                ltac:(M.monadic
                                  (let~ _ :=
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::iterator::Iterator",
                                            Ty.apply
                                              (Ty.path "core::ops::range::Range")
                                              []
                                              [ Ty.path "usize" ],
                                            [],
                                            "next",
                                            []
                                          |),
                                          [ iter ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let _ :=
                                              M.is_struct_tuple (|
                                                γ,
                                                "core::option::Option::None"
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (| M.read (| M.break (||) |) |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::option::Option::Some",
                                                0
                                              |) in
                                            let idx := M.copy (| γ0_0 |) in
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ :=
                                                      M.use
                                                        (M.alloc (|
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::cmp::PartialEq",
                                                              A,
                                                              [ B ],
                                                              "ne",
                                                              []
                                                            |),
                                                            [
                                                              M.SubPointer.get_array_field (|
                                                                M.read (| self |),
                                                                idx
                                                              |);
                                                              M.SubPointer.get_array_field (|
                                                                M.read (| other |),
                                                                idx
                                                              |)
                                                            ]
                                                          |)
                                                        |)) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          M.return_ (| Value.Bool false |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                              |)))
                        ]
                      |)) in
                  M.alloc (| Value.Bool true |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (A B : Ty.t),
        M.IsTraitInstance
          "core::slice::cmp::SlicePartialEq"
          (Self A B)
          (* Trait polymorphic types *) [ (* B *) B ]
          (* Instance *) [ ("equal", InstanceField.Method (equal A B)) ].
    End Impl_core_slice_cmp_SlicePartialEq_where_core_cmp_PartialEq_A_B_B_for_slice_A.
    
    Module Impl_core_slice_cmp_SlicePartialEq_where_core_cmp_bytewise_BytewiseEq_A_B_B_for_slice_A.
      Definition Self (A B : Ty.t) : Ty.t := Ty.apply (Ty.path "slice") [] [ A ].
      
      (*
          fn equal(&self, other: &[B]) -> bool {
              if self.len() != other.len() {
                  return false;
              }
      
              // SAFETY: `self` and `other` are references and are thus guaranteed to be valid.
              // The two slices have been checked to have the same size above.
              unsafe {
                  let size = mem::size_of_val(self);
                  compare_bytes(self.as_ptr() as *const u8, other.as_ptr() as *const u8, size) == 0
              }
          }
      *)
      Definition equal (A B : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A B in
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ne (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ A ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |),
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ B ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| other |) ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (| M.read (| M.return_ (| Value.Bool false |) |) |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ size :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::mem::size_of_val",
                          [ Ty.apply (Ty.path "slice") [] [ A ] ]
                        |),
                        [ M.read (| self |) ]
                      |)
                    |) in
                  M.alloc (|
                    BinOp.eq (|
                      M.call_closure (|
                        M.get_function (| "core::intrinsics::compare_bytes", [] |),
                        [
                          M.rust_cast
                            (M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ A ],
                                "as_ptr",
                                []
                              |),
                              [ M.read (| self |) ]
                            |));
                          M.rust_cast
                            (M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ B ],
                                "as_ptr",
                                []
                              |),
                              [ M.read (| other |) ]
                            |));
                          M.read (| size |)
                        ]
                      |),
                      Value.Integer IntegerKind.I32 0
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (A B : Ty.t),
        M.IsTraitInstance
          "core::slice::cmp::SlicePartialEq"
          (Self A B)
          (* Trait polymorphic types *) [ (* B *) B ]
          (* Instance *) [ ("equal", InstanceField.Method (equal A B)) ].
    End Impl_core_slice_cmp_SlicePartialEq_where_core_cmp_bytewise_BytewiseEq_A_B_B_for_slice_A.
    
    (* Trait *)
    (* Empty module 'SlicePartialOrd' *)
    
    Module Impl_core_slice_cmp_SlicePartialOrd_where_core_cmp_PartialOrd_A_for_A.
      Definition Self (A : Ty.t) : Ty.t := A.
      
      (*
          default fn partial_compare(left: &[A], right: &[A]) -> Option<Ordering> {
              let l = cmp::min(left.len(), right.len());
      
              // Slice to the loop iteration range to enable bound check
              // elimination in the compiler
              let lhs = &left[..l];
              let rhs = &right[..l];
      
              for i in 0..l {
                  match lhs[i].partial_cmp(&rhs[i]) {
                      Some(Ordering::Equal) => (),
                      non_eq => return non_eq,
                  }
              }
      
              left.len().partial_cmp(&right.len())
          }
      *)
      Definition partial_compare
          (A : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self A in
        match ε, τ, α with
        | [], [], [ _ as left; _ as right ] =>
          ltac:(M.monadic
            (let left := M.alloc (| left |) in
            let right := M.alloc (| right |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ l :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::cmp::min", [ Ty.path "usize" ] |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ A ],
                              "len",
                              []
                            |),
                            [ M.read (| left |) ]
                          |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ A ],
                              "len",
                              []
                            |),
                            [ M.read (| right |) ]
                          |)
                        ]
                      |)
                    |) in
                  let~ lhs :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::index::Index",
                          Ty.apply (Ty.path "slice") [] [ A ],
                          [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ],
                          "index",
                          []
                        |),
                        [
                          M.read (| left |);
                          Value.StructRecord
                            "core::ops::range::RangeTo"
                            [ ("end_", M.read (| l |)) ]
                        ]
                      |)
                    |) in
                  let~ rhs :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::index::Index",
                          Ty.apply (Ty.path "slice") [] [ A ],
                          [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ],
                          "index",
                          []
                        |),
                        [
                          M.read (| right |);
                          Value.StructRecord
                            "core::ops::range::RangeTo"
                            [ ("end_", M.read (| l |)) ]
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.use
                      (M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::collect::IntoIterator",
                              Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                              [],
                              "into_iter",
                              []
                            |),
                            [
                              Value.StructRecord
                                "core::ops::range::Range"
                                [
                                  ("start", Value.Integer IntegerKind.Usize 0);
                                  ("end_", M.read (| l |))
                                ]
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let iter := M.copy (| γ |) in
                              M.loop (|
                                ltac:(M.monadic
                                  (let~ _ :=
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::iterator::Iterator",
                                            Ty.apply
                                              (Ty.path "core::ops::range::Range")
                                              []
                                              [ Ty.path "usize" ],
                                            [],
                                            "next",
                                            []
                                          |),
                                          [ iter ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let _ :=
                                              M.is_struct_tuple (|
                                                γ,
                                                "core::option::Option::None"
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (| M.read (| M.break (||) |) |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::option::Option::Some",
                                                0
                                              |) in
                                            let i := M.copy (| γ0_0 |) in
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::cmp::PartialOrd",
                                                    A,
                                                    [ A ],
                                                    "partial_cmp",
                                                    []
                                                  |),
                                                  [
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| lhs |),
                                                      i
                                                    |);
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| rhs |),
                                                      i
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::option::Option::Some",
                                                        0
                                                      |) in
                                                    let _ :=
                                                      M.is_struct_tuple (|
                                                        γ0_0,
                                                        "core::cmp::Ordering::Equal"
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let non_eq := M.copy (| γ |) in
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          M.return_ (| M.read (| non_eq |) |)
                                                        |)
                                                      |)
                                                    |)))
                                              ]
                                            |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                              |)))
                        ]
                      |)) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialOrd",
                        Ty.path "usize",
                        [ Ty.path "usize" ],
                        "partial_cmp",
                        []
                      |),
                      [
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ A ],
                              "len",
                              []
                            |),
                            [ M.read (| left |) ]
                          |)
                        |);
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ A ],
                              "len",
                              []
                            |),
                            [ M.read (| right |) ]
                          |)
                        |)
                      ]
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (A : Ty.t),
        M.IsTraitInstance
          "core::slice::cmp::SlicePartialOrd"
          (Self A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("partial_compare", InstanceField.Method (partial_compare A)) ].
    End Impl_core_slice_cmp_SlicePartialOrd_where_core_cmp_PartialOrd_A_for_A.
    
    Module Impl_core_slice_cmp_SlicePartialOrd_where_core_slice_cmp_AlwaysApplicableOrd_A_for_A.
      Definition Self (A : Ty.t) : Ty.t := A.
      
      (*
          fn partial_compare(left: &[A], right: &[A]) -> Option<Ordering> {
              Some(SliceOrd::compare(left, right))
          }
      *)
      Definition partial_compare
          (A : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self A in
        match ε, τ, α with
        | [], [], [ _ as left; _ as right ] =>
          ltac:(M.monadic
            (let left := M.alloc (| left |) in
            let right := M.alloc (| right |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_trait_method (| "core::slice::cmp::SliceOrd", A, [], "compare", [] |),
                  [ M.read (| left |); M.read (| right |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (A : Ty.t),
        M.IsTraitInstance
          "core::slice::cmp::SlicePartialOrd"
          (Self A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("partial_compare", InstanceField.Method (partial_compare A)) ].
    End Impl_core_slice_cmp_SlicePartialOrd_where_core_slice_cmp_AlwaysApplicableOrd_A_for_A.
    
    (* Trait *)
    (* Empty module 'AlwaysApplicableOrd' *)
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_for_u8.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_for_u16.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_for_u32.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_for_u64.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_for_u128.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_for_usize.
      Definition Self : Ty.t := Ty.path "usize".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_for_usize.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_for_i8.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_for_i16.
      Definition Self : Ty.t := Ty.path "i16".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_for_i16.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_for_i32.
      Definition Self : Ty.t := Ty.path "i32".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_for_i32.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_for_i64.
      Definition Self : Ty.t := Ty.path "i64".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_for_i64.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_for_i128.
      Definition Self : Ty.t := Ty.path "i128".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_for_i128.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_for_isize.
      Definition Self : Ty.t := Ty.path "isize".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_for_isize.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_for_bool.
      Definition Self : Ty.t := Ty.path "bool".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_for_bool.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_for_char.
      Definition Self : Ty.t := Ty.path "char".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_for_char.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_where_core_marker_Sized_T_for_pointer_const_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*const") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_where_core_marker_Sized_T_for_pointer_const_T.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_where_core_marker_Sized_T_for_pointer_mut_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "*mut") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_where_core_marker_Sized_T_for_pointer_mut_T.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_where_core_slice_cmp_AlwaysApplicableOrd_T_for_ref__T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_where_core_slice_cmp_AlwaysApplicableOrd_T_for_ref__T.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_where_core_slice_cmp_AlwaysApplicableOrd_T_for_ref_mut_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_where_core_slice_cmp_AlwaysApplicableOrd_T_for_ref_mut_T.
    
    Module Impl_core_slice_cmp_AlwaysApplicableOrd_where_core_slice_cmp_AlwaysApplicableOrd_T_for_core_option_Option_T.
      Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::cmp::AlwaysApplicableOrd"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_AlwaysApplicableOrd_where_core_slice_cmp_AlwaysApplicableOrd_T_for_core_option_Option_T.
    
    (* Trait *)
    (* Empty module 'SliceOrd' *)
    
    Module Impl_core_slice_cmp_SliceOrd_where_core_cmp_Ord_A_for_A.
      Definition Self (A : Ty.t) : Ty.t := A.
      
      (*
          default fn compare(left: &[Self], right: &[Self]) -> Ordering {
              let l = cmp::min(left.len(), right.len());
      
              // Slice to the loop iteration range to enable bound check
              // elimination in the compiler
              let lhs = &left[..l];
              let rhs = &right[..l];
      
              for i in 0..l {
                  match lhs[i].cmp(&rhs[i]) {
                      Ordering::Equal => (),
                      non_eq => return non_eq,
                  }
              }
      
              left.len().cmp(&right.len())
          }
      *)
      Definition compare (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A in
        match ε, τ, α with
        | [], [], [ _ as left; _ as right ] =>
          ltac:(M.monadic
            (let left := M.alloc (| left |) in
            let right := M.alloc (| right |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ l :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::cmp::min", [ Ty.path "usize" ] |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ A ],
                              "len",
                              []
                            |),
                            [ M.read (| left |) ]
                          |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ A ],
                              "len",
                              []
                            |),
                            [ M.read (| right |) ]
                          |)
                        ]
                      |)
                    |) in
                  let~ lhs :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::index::Index",
                          Ty.apply (Ty.path "slice") [] [ A ],
                          [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ],
                          "index",
                          []
                        |),
                        [
                          M.read (| left |);
                          Value.StructRecord
                            "core::ops::range::RangeTo"
                            [ ("end_", M.read (| l |)) ]
                        ]
                      |)
                    |) in
                  let~ rhs :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::index::Index",
                          Ty.apply (Ty.path "slice") [] [ A ],
                          [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ],
                          "index",
                          []
                        |),
                        [
                          M.read (| right |);
                          Value.StructRecord
                            "core::ops::range::RangeTo"
                            [ ("end_", M.read (| l |)) ]
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.use
                      (M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::collect::IntoIterator",
                              Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                              [],
                              "into_iter",
                              []
                            |),
                            [
                              Value.StructRecord
                                "core::ops::range::Range"
                                [
                                  ("start", Value.Integer IntegerKind.Usize 0);
                                  ("end_", M.read (| l |))
                                ]
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let iter := M.copy (| γ |) in
                              M.loop (|
                                ltac:(M.monadic
                                  (let~ _ :=
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::iterator::Iterator",
                                            Ty.apply
                                              (Ty.path "core::ops::range::Range")
                                              []
                                              [ Ty.path "usize" ],
                                            [],
                                            "next",
                                            []
                                          |),
                                          [ iter ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let _ :=
                                              M.is_struct_tuple (|
                                                γ,
                                                "core::option::Option::None"
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (| M.read (| M.break (||) |) |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::option::Option::Some",
                                                0
                                              |) in
                                            let i := M.copy (| γ0_0 |) in
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::cmp::Ord",
                                                    A,
                                                    [],
                                                    "cmp",
                                                    []
                                                  |),
                                                  [
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| lhs |),
                                                      i
                                                    |);
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| rhs |),
                                                      i
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let _ :=
                                                      M.is_struct_tuple (|
                                                        γ,
                                                        "core::cmp::Ordering::Equal"
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let non_eq := M.copy (| γ |) in
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          M.return_ (| M.read (| non_eq |) |)
                                                        |)
                                                      |)
                                                    |)))
                                              ]
                                            |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                              |)))
                        ]
                      |)) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (| "core::cmp::Ord", Ty.path "usize", [], "cmp", [] |),
                      [
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ A ],
                              "len",
                              []
                            |),
                            [ M.read (| left |) ]
                          |)
                        |);
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ A ],
                              "len",
                              []
                            |),
                            [ M.read (| right |) ]
                          |)
                        |)
                      ]
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (A : Ty.t),
        M.IsTraitInstance
          "core::slice::cmp::SliceOrd"
          (Self A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("compare", InstanceField.Method (compare A)) ].
    End Impl_core_slice_cmp_SliceOrd_where_core_cmp_Ord_A_for_A.
    
    (* Trait *)
    (* Empty module 'UnsignedBytewiseOrd' *)
    
    Module Impl_core_slice_cmp_UnsignedBytewiseOrd_for_bool.
      Definition Self : Ty.t := Ty.path "bool".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::UnsignedBytewiseOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_UnsignedBytewiseOrd_for_bool.
    
    Module Impl_core_slice_cmp_UnsignedBytewiseOrd_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::UnsignedBytewiseOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_UnsignedBytewiseOrd_for_u8.
    
    Module Impl_core_slice_cmp_UnsignedBytewiseOrd_for_core_num_nonzero_NonZero_u8.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u8" ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::UnsignedBytewiseOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_UnsignedBytewiseOrd_for_core_num_nonzero_NonZero_u8.
    
    Module Impl_core_slice_cmp_UnsignedBytewiseOrd_for_core_option_Option_core_num_nonzero_NonZero_u8.
      Definition Self : Ty.t :=
        Ty.apply
          (Ty.path "core::option::Option")
          []
          [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u8" ] ].
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::UnsignedBytewiseOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_UnsignedBytewiseOrd_for_core_option_Option_core_num_nonzero_NonZero_u8.
    
    Module Impl_core_slice_cmp_UnsignedBytewiseOrd_for_core_ascii_ascii_char_AsciiChar.
      Definition Self : Ty.t := Ty.path "core::ascii::ascii_char::AsciiChar".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::UnsignedBytewiseOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_slice_cmp_UnsignedBytewiseOrd_for_core_ascii_ascii_char_AsciiChar.
    
    Module Impl_core_slice_cmp_SliceOrd_where_core_cmp_Ord_A_where_core_slice_cmp_UnsignedBytewiseOrd_A_for_A.
      Definition Self (A : Ty.t) : Ty.t := A.
      
      (*
          fn compare(left: &[Self], right: &[Self]) -> Ordering {
              // Since the length of a slice is always less than or equal to
              // isize::MAX, this never underflows.
              let diff = left.len() as isize - right.len() as isize;
              // This comparison gets optimized away (on x86_64 and ARM) because the
              // subtraction updates flags.
              let len = if left.len() < right.len() { left.len() } else { right.len() };
              let left = left.as_ptr().cast();
              let right = right.as_ptr().cast();
              // SAFETY: `left` and `right` are references and are thus guaranteed to
              // be valid. `UnsignedBytewiseOrd` is only implemented for types that
              // are valid u8s and can be compared the same way. We use the minimum
              // of both lengths which guarantees that both regions are valid for
              // reads in that interval.
              let mut order = unsafe { compare_bytes(left, right, len) as isize };
              if order == 0 {
                  order = diff;
              }
              order.cmp(&0)
          }
      *)
      Definition compare (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self A in
        match ε, τ, α with
        | [], [], [ _ as left; _ as right ] =>
          ltac:(M.monadic
            (let left := M.alloc (| left |) in
            let right := M.alloc (| right |) in
            M.read (|
              let~ diff :=
                M.alloc (|
                  BinOp.Wrap.sub (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ A ],
                          "len",
                          []
                        |),
                        [ M.read (| left |) ]
                      |)),
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ A ],
                          "len",
                          []
                        |),
                        [ M.read (| right |) ]
                      |))
                  |)
                |) in
              let~ len :=
                M.copy (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ A ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| left |) ]
                                  |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ A ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| right |) ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ A ],
                                "len",
                                []
                              |),
                              [ M.read (| left |) ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ A ],
                                "len",
                                []
                              |),
                              [ M.read (| right |) ]
                            |)
                          |)))
                    ]
                  |)
                |) in
              let~ left :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "*const") [] [ A ],
                      "cast",
                      [ Ty.path "u8" ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ A ],
                          "as_ptr",
                          []
                        |),
                        [ M.read (| left |) ]
                      |)
                    ]
                  |)
                |) in
              let~ right :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "*const") [] [ A ],
                      "cast",
                      [ Ty.path "u8" ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ A ],
                          "as_ptr",
                          []
                        |),
                        [ M.read (| right |) ]
                      |)
                    ]
                  |)
                |) in
              let~ order :=
                M.alloc (|
                  M.rust_cast
                    (M.call_closure (|
                      M.get_function (| "core::intrinsics::compare_bytes", [] |),
                      [ M.read (| left |); M.read (| right |); M.read (| len |) ]
                    |))
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.eq (| M.read (| order |), Value.Integer IntegerKind.Isize 0 |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ := M.write (| order, M.read (| diff |) |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::cmp::Ord", Ty.path "isize", [], "cmp", [] |),
                  [ order; M.alloc (| Value.Integer IntegerKind.Isize 0 |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (A : Ty.t),
        M.IsTraitInstance
          "core::slice::cmp::SliceOrd"
          (Self A)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("compare", InstanceField.Method (compare A)) ].
    End Impl_core_slice_cmp_SliceOrd_where_core_cmp_Ord_A_where_core_slice_cmp_UnsignedBytewiseOrd_A_for_A.
    
    (* Trait *)
    (* Empty module 'SliceContains' *)
    
    Module Impl_core_slice_cmp_SliceContains_where_core_cmp_PartialEq_T_for_T.
      Definition Self (T : Ty.t) : Ty.t := T.
      
      (*
          default fn slice_contains(&self, x: &[Self]) -> bool {
              x.iter().any(|y| *y == *self)
          }
      *)
      Definition slice_contains
          (T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self T in
        match ε, τ, α with
        | [], [], [ self; x ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let x := M.alloc (| x |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                [],
                "any",
                [ Ty.function [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ] (Ty.path "bool") ]
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.apply (Ty.path "slice") [] [ T ], "iter", [] |),
                    [ M.read (| x |) ]
                  |)
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let y := M.copy (| γ |) in
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialEq",
                                      T,
                                      [ T ],
                                      "eq",
                                      []
                                    |),
                                    [ M.read (| y |); M.read (| self |) ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (T : Ty.t),
        M.IsTraitInstance
          "core::slice::cmp::SliceContains"
          (Self T)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("slice_contains", InstanceField.Method (slice_contains T)) ].
    End Impl_core_slice_cmp_SliceContains_where_core_cmp_PartialEq_T_for_T.
    
    Module Impl_core_slice_cmp_SliceContains_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*
          fn slice_contains(&self, x: &[Self]) -> bool {
              memchr::memchr( *self, x).is_some()
          }
      *)
      Definition slice_contains (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; x ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let x := M.alloc (| x |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ],
                "is_some",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::slice::memchr::memchr", [] |),
                    [ M.read (| M.read (| self |) |); M.read (| x |) ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::SliceContains"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("slice_contains", InstanceField.Method slice_contains) ].
    End Impl_core_slice_cmp_SliceContains_for_u8.
    
    Module Impl_core_slice_cmp_SliceContains_for_i8.
      Definition Self : Ty.t := Ty.path "i8".
      
      (*
          fn slice_contains(&self, x: &[Self]) -> bool {
              let byte = *self as u8;
              // SAFETY: `i8` and `u8` have the same memory layout, thus casting `x.as_ptr()`
              // as `*const u8` is safe. The `x.as_ptr()` comes from a reference and is thus guaranteed
              // to be valid for reads for the length of the slice `x.len()`, which cannot be larger
              // than `isize::MAX`. The returned slice is never mutated.
              let bytes: &[u8] = unsafe { from_raw_parts(x.as_ptr() as *const u8, x.len()) };
              memchr::memchr(byte, bytes).is_some()
          }
      *)
      Definition slice_contains (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; x ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let x := M.alloc (| x |) in
            M.read (|
              let~ byte := M.alloc (| M.rust_cast (M.read (| M.read (| self |) |)) |) in
              let~ bytes :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::slice::raw::from_raw_parts", [ Ty.path "u8" ] |),
                    [
                      M.rust_cast
                        (M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ Ty.path "i8" ],
                            "as_ptr",
                            []
                          |),
                          [ M.read (| x |) ]
                        |));
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "i8" ],
                          "len",
                          []
                        |),
                        [ M.read (| x |) ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ],
                    "is_some",
                    []
                  |),
                  [
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "core::slice::memchr::memchr", [] |),
                        [ M.read (| byte |); M.read (| bytes |) ]
                      |)
                    |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::cmp::SliceContains"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("slice_contains", InstanceField.Method slice_contains) ].
    End Impl_core_slice_cmp_SliceContains_for_i8.
  End cmp.
End slice.
