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

Module str.
  Module traits.
    Module Impl_core_cmp_Ord_for_str.
      Definition Self : Ty.t := Ty.path "str".
      
      (*
          fn cmp(&self, other: &str) -> Ordering {
              self.as_bytes().cmp(other.as_bytes())
          }
      *)
      Definition cmp (ε : 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.call_closure (|
              M.get_trait_method (|
                "core::cmp::Ord",
                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                [],
                "cmp",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                  [ M.read (| self |) ]
                |);
                M.call_closure (|
                  M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                  [ M.read (| other |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_str.
    
    Module Impl_core_cmp_PartialEq_for_str.
      Definition Self : Ty.t := Ty.path "str".
      
      (*
          fn eq(&self, other: &str) -> bool {
              self.as_bytes() == other.as_bytes()
          }
      *)
      Definition eq (ε : 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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ] ],
                "eq",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                    [ M.read (| self |) ]
                  |)
                |);
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "str", "as_bytes", [] |),
                    [ M.read (| other |) ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_str.
    
    Module Impl_core_cmp_Eq_for_str.
      Definition Self : Ty.t := Ty.path "str".
      
      Axiom Implements :
        M.IsTraitInstance "core::cmp::Eq" Self (* Trait polymorphic types *) [] (* Instance *) [].
    End Impl_core_cmp_Eq_for_str.
    
    Module Impl_core_cmp_PartialOrd_for_str.
      Definition Self : Ty.t := Ty.path "str".
      
      (*
          fn partial_cmp(&self, other: &str) -> Option<Ordering> {
              Some(self.cmp(other))
          }
      *)
      Definition partial_cmp (ε : 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
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_trait_method (| "core::cmp::Ord", Ty.path "str", [], "cmp", [] |),
                  [ M.read (| self |); M.read (| other |) ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
    End Impl_core_cmp_PartialOrd_for_str.
    
    Module Impl_core_ops_index_Index_where_core_slice_index_SliceIndex_I_str_I_for_str.
      Definition Self (I : Ty.t) : Ty.t := Ty.path "str".
      
      (*     type Output = I::Output; *)
      Definition _Output (I : Ty.t) : Ty.t := Ty.associated.
      
      (*
          fn index(&self, index: I) -> &I::Output {
              index.index(self)
          }
      *)
      Definition index (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self I in
        match ε, τ, α with
        | [], [], [ self; index ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let index := M.alloc (| index |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                I,
                [ Ty.path "str" ],
                "index",
                []
              |),
              [ M.read (| index |); M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (I : Ty.t),
        M.IsTraitInstance
          "core::ops::index::Index"
          (Self I)
          (* Trait polymorphic types *) [ (* Idx *) I ]
          (* Instance *)
          [ ("Output", InstanceField.Ty (_Output I)); ("index", InstanceField.Method (index I)) ].
    End Impl_core_ops_index_Index_where_core_slice_index_SliceIndex_I_str_I_for_str.
    
    Module Impl_core_ops_index_IndexMut_where_core_slice_index_SliceIndex_I_str_I_for_str.
      Definition Self (I : Ty.t) : Ty.t := Ty.path "str".
      
      (*
          fn index_mut(&mut self, index: I) -> &mut I::Output {
              index.index_mut(self)
          }
      *)
      Definition index_mut (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self I in
        match ε, τ, α with
        | [], [], [ self; index ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let index := M.alloc (| index |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                I,
                [ Ty.path "str" ],
                "index_mut",
                []
              |),
              [ M.read (| index |); M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (I : Ty.t),
        M.IsTraitInstance
          "core::ops::index::IndexMut"
          (Self I)
          (* Trait polymorphic types *) [ (* Idx *) I ]
          (* Instance *) [ ("index_mut", InstanceField.Method (index_mut I)) ].
    End Impl_core_ops_index_IndexMut_where_core_slice_index_SliceIndex_I_str_I_for_str.
    
    (*
    const fn str_index_overflow_fail() -> ! {
        panic!("attempted to index str up to maximum usize");
    }
    *)
    Definition str_index_overflow_fail (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.call_closure (|
            M.get_function (| "core::panicking::panic_fmt", [] |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                [
                  M.alloc (|
                    Value.Array
                      [ M.read (| Value.String "attempted to index str up to maximum usize" |) ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_str_index_overflow_fail :
      M.IsFunction "core::str::traits::str_index_overflow_fail" str_index_overflow_fail.
    
    Module Impl_core_slice_index_SliceIndex_str_for_core_ops_range_RangeFull.
      Definition Self : Ty.t := Ty.path "core::ops::range::RangeFull".
      
      (*     type Output = str; *)
      Definition _Output : Ty.t := Ty.path "str".
      
      (*
          fn get(self, slice: &str) -> Option<&Self::Output> {
              Some(slice)
          }
      *)
      Definition get (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            Value.StructTuple "core::option::Option::Some" [ M.read (| slice |) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut str) -> Option<&mut Self::Output> {
              Some(slice)
          }
      *)
      Definition get_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            Value.StructTuple "core::option::Option::Some" [ M.read (| slice |) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const str) -> *const Self::Output {
              slice
          }
      *)
      Definition get_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (| slice |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut str) -> *mut Self::Output {
              slice
          }
      *)
      Definition get_unchecked_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (| slice |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &str) -> &Self::Output {
              slice
          }
      *)
      Definition index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (| slice |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut str) -> &mut Self::Output {
              slice
          }
      *)
      Definition index_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (| slice |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "str" ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty _Output);
            ("get", InstanceField.Method get);
            ("get_mut", InstanceField.Method get_mut);
            ("get_unchecked", InstanceField.Method get_unchecked);
            ("get_unchecked_mut", InstanceField.Method get_unchecked_mut);
            ("index", InstanceField.Method index);
            ("index_mut", InstanceField.Method index_mut)
          ].
    End Impl_core_slice_index_SliceIndex_str_for_core_ops_range_RangeFull.
    
    Module Impl_core_slice_index_SliceIndex_str_for_core_ops_range_Range_usize.
      Definition Self : Ty.t := Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ].
      
      (*     type Output = str; *)
      Definition _Output : Ty.t := Ty.path "str".
      
      (*
          fn get(self, slice: &str) -> Option<&Self::Output> {
              if self.start <= self.end
                  && slice.is_char_boundary(self.start)
                  && slice.is_char_boundary(self.end)
              {
                  // SAFETY: just checked that `start` and `end` are on a char boundary,
                  // and we are passing in a safe reference, so the return value will also be one.
                  // We also checked char boundaries, so this is valid UTF-8.
                  Some(unsafe { &*self.get_unchecked(slice) })
              } else {
                  None
              }
          }
      *)
      Definition get (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            LogicalOp.and (|
                              LogicalOp.and (|
                                BinOp.le (|
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      self,
                                      "core::ops::range::Range",
                                      "start"
                                    |)
                                  |),
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      self,
                                      "core::ops::range::Range",
                                      "end"
                                    |)
                                  |)
                                |),
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "str",
                                      "is_char_boundary",
                                      []
                                    |),
                                    [
                                      M.read (| slice |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          self,
                                          "core::ops::range::Range",
                                          "start"
                                        |)
                                      |)
                                    ]
                                  |)))
                              |),
                              ltac:(M.monadic
                                (M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "str",
                                    "is_char_boundary",
                                    []
                                  |),
                                  [
                                    M.read (| slice |);
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        self,
                                        "core::ops::range::Range",
                                        "end"
                                      |)
                                    |)
                                  ]
                                |)))
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::slice::index::SliceIndex",
                                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                                [ Ty.path "str" ],
                                "get_unchecked",
                                []
                              |),
                              [ M.read (| self |); M.read (| slice |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut str) -> Option<&mut Self::Output> {
              if self.start <= self.end
                  && slice.is_char_boundary(self.start)
                  && slice.is_char_boundary(self.end)
              {
                  // SAFETY: just checked that `start` and `end` are on a char boundary.
                  // We know the pointer is unique because we got it from `slice`.
                  Some(unsafe { &mut *self.get_unchecked_mut(slice) })
              } else {
                  None
              }
          }
      *)
      Definition get_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            LogicalOp.and (|
                              LogicalOp.and (|
                                BinOp.le (|
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      self,
                                      "core::ops::range::Range",
                                      "start"
                                    |)
                                  |),
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      self,
                                      "core::ops::range::Range",
                                      "end"
                                    |)
                                  |)
                                |),
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "str",
                                      "is_char_boundary",
                                      []
                                    |),
                                    [
                                      M.read (| slice |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          self,
                                          "core::ops::range::Range",
                                          "start"
                                        |)
                                      |)
                                    ]
                                  |)))
                              |),
                              ltac:(M.monadic
                                (M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "str",
                                    "is_char_boundary",
                                    []
                                  |),
                                  [
                                    M.read (| slice |);
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        self,
                                        "core::ops::range::Range",
                                        "end"
                                      |)
                                    |)
                                  ]
                                |)))
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::slice::index::SliceIndex",
                                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                                [ Ty.path "str" ],
                                "get_unchecked_mut",
                                []
                              |),
                              [ M.read (| self |); M.read (| slice |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const str) -> *const Self::Output {
              let slice = slice as *const [u8];
      
              assert_unsafe_precondition!(
                  // We'd like to check that the bounds are on char boundaries,
                  // but there's not really a way to do so without reading
                  // behind the pointer, which has aliasing implications.
                  // It's also not possible to move this check up to
                  // `str::get_unchecked` without adding a special function
                  // to `SliceIndex` just for this.
                  check_library_ub,
                  "str::get_unchecked requires that the range is within the string slice",
                  (
                      start: usize = self.start,
                      end: usize = self.end,
                      len: usize = slice.len()
                  ) => end >= start && end <= len,
              );
      
              // SAFETY: the caller guarantees that `self` is in bounds of `slice`
              // which satisfies all the conditions for `add`.
              unsafe {
                  let new_len = unchecked_sub(self.end, self.start);
                  ptr::slice_from_raw_parts(slice.as_ptr().add(self.start), new_len) as *const str
              }
          }
      *)
      Definition get_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ slice := M.alloc (| M.rust_cast (M.read (| slice |)) |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::ub_checks", [] |),
                                []
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Self,
                                "precondition_check.get_unchecked",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::Range",
                                    "start"
                                  |)
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::Range",
                                    "end"
                                  |)
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "*const")
                                      []
                                      [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ new_len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::unchecked_sub", [ Ty.path "usize" ] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::Range",
                          "end"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::Range",
                          "start"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.rust_cast
                  (M.call_closure (|
                    M.get_function (| "core::ptr::slice_from_raw_parts", [ Ty.path "u8" ] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                          "add",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "*const")
                                []
                                [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                              "as_ptr",
                              []
                            |),
                            [ M.read (| slice |) ]
                          |);
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "core::ops::range::Range",
                              "start"
                            |)
                          |)
                        ]
                      |);
                      M.read (| new_len |)
                    ]
                  |))
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut str) -> *mut Self::Output {
              let slice = slice as *mut [u8];
      
              assert_unsafe_precondition!(
                  check_library_ub,
                  "str::get_unchecked_mut requires that the range is within the string slice",
                  (
                      start: usize = self.start,
                      end: usize = self.end,
                      len: usize = slice.len()
                  ) => end >= start && end <= len,
              );
      
              // SAFETY: see comments for `get_unchecked`.
              unsafe {
                  let new_len = unchecked_sub(self.end, self.start);
                  ptr::slice_from_raw_parts_mut(slice.as_mut_ptr().add(self.start), new_len) as *mut str
              }
          }
      *)
      Definition get_unchecked_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ slice := M.alloc (| M.rust_cast (M.read (| slice |)) |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::ub_checks", [] |),
                                []
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Self,
                                "precondition_check.get_unchecked_mut",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::Range",
                                    "start"
                                  |)
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::Range",
                                    "end"
                                  |)
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "*mut")
                                      []
                                      [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ new_len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::unchecked_sub", [ Ty.path "usize" ] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::Range",
                          "end"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::Range",
                          "start"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.rust_cast
                  (M.call_closure (|
                    M.get_function (| "core::ptr::slice_from_raw_parts_mut", [ Ty.path "u8" ] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*mut") [] [ Ty.path "u8" ],
                          "add",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "*mut")
                                []
                                [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                              "as_mut_ptr",
                              []
                            |),
                            [ M.read (| slice |) ]
                          |);
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "core::ops::range::Range",
                              "start"
                            |)
                          |)
                        ]
                      |);
                      M.read (| new_len |)
                    ]
                  |))
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &str) -> &Self::Output {
              let (start, end) = (self.start, self.end);
              match self.get(slice) {
                  Some(s) => s,
                  None => super::slice_error_fail(slice, start, end),
              }
          }
      *)
      Definition index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  Value.Tuple
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::Range",
                          "start"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::Range",
                          "end"
                        |)
                      |)
                    ]
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let start := M.copy (| γ0_0 |) in
                      let end_ := M.copy (| γ0_1 |) in
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::slice::index::SliceIndex",
                              Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                              [ Ty.path "str" ],
                              "get",
                              []
                            |),
                            [ M.read (| self |); M.read (| slice |) ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let s := M.copy (| γ0_0 |) in
                              M.alloc (| M.read (| s |) |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.call_closure (|
                                    M.get_function (| "core::str::slice_error_fail", [] |),
                                    [ M.read (| slice |); M.read (| start |); M.read (| end_ |) ]
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut str) -> &mut Self::Output {
              // is_char_boundary checks that the index is in [0, .len()]
              // cannot reuse `get` as above, because of NLL trouble
              if self.start <= self.end
                  && slice.is_char_boundary(self.start)
                  && slice.is_char_boundary(self.end)
              {
                  // SAFETY: just checked that `start` and `end` are on a char boundary,
                  // and we are passing in a safe reference, so the return value will also be one.
                  unsafe { &mut *self.get_unchecked_mut(slice) }
              } else {
                  super::slice_error_fail(slice, self.start, self.end)
              }
          }
      *)
      Definition index_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            LogicalOp.and (|
                              LogicalOp.and (|
                                BinOp.le (|
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      self,
                                      "core::ops::range::Range",
                                      "start"
                                    |)
                                  |),
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      self,
                                      "core::ops::range::Range",
                                      "end"
                                    |)
                                  |)
                                |),
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "str",
                                      "is_char_boundary",
                                      []
                                    |),
                                    [
                                      M.read (| slice |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          self,
                                          "core::ops::range::Range",
                                          "start"
                                        |)
                                      |)
                                    ]
                                  |)))
                              |),
                              ltac:(M.monadic
                                (M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "str",
                                    "is_char_boundary",
                                    []
                                  |),
                                  [
                                    M.read (| slice |);
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        self,
                                        "core::ops::range::Range",
                                        "end"
                                      |)
                                    |)
                                  ]
                                |)))
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::slice::index::SliceIndex",
                            Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                            [ Ty.path "str" ],
                            "get_unchecked_mut",
                            []
                          |),
                          [ M.read (| self |); M.read (| slice |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::str::slice_error_fail", [] |),
                            [
                              M.read (| slice |);
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::ops::range::Range",
                                  "start"
                                |)
                              |);
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::ops::range::Range",
                                  "end"
                                |)
                              |)
                            ]
                          |)
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "str" ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty _Output);
            ("get", InstanceField.Method get);
            ("get_mut", InstanceField.Method get_mut);
            ("get_unchecked", InstanceField.Method get_unchecked);
            ("get_unchecked_mut", InstanceField.Method get_unchecked_mut);
            ("index", InstanceField.Method index);
            ("index_mut", InstanceField.Method index_mut)
          ].
    End Impl_core_slice_index_SliceIndex_str_for_core_ops_range_Range_usize.
    
    Module Impl_core_slice_index_SliceIndex_str_for_core_range_Range_usize.
      Definition Self : Ty.t := Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ].
      
      (*     type Output = str; *)
      Definition _Output : Ty.t := Ty.path "str".
      
      (*
          fn get(self, slice: &str) -> Option<&Self::Output> {
              if self.start <= self.end
                  && slice.is_char_boundary(self.start)
                  && slice.is_char_boundary(self.end)
              {
                  // SAFETY: just checked that `start` and `end` are on a char boundary,
                  // and we are passing in a safe reference, so the return value will also be one.
                  // We also checked char boundaries, so this is valid UTF-8.
                  Some(unsafe { &*self.get_unchecked(slice) })
              } else {
                  None
              }
          }
      *)
      Definition get (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            LogicalOp.and (|
                              LogicalOp.and (|
                                BinOp.le (|
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      self,
                                      "core::range::Range",
                                      "start"
                                    |)
                                  |),
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      self,
                                      "core::range::Range",
                                      "end"
                                    |)
                                  |)
                                |),
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "str",
                                      "is_char_boundary",
                                      []
                                    |),
                                    [
                                      M.read (| slice |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          self,
                                          "core::range::Range",
                                          "start"
                                        |)
                                      |)
                                    ]
                                  |)))
                              |),
                              ltac:(M.monadic
                                (M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "str",
                                    "is_char_boundary",
                                    []
                                  |),
                                  [
                                    M.read (| slice |);
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        self,
                                        "core::range::Range",
                                        "end"
                                      |)
                                    |)
                                  ]
                                |)))
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::slice::index::SliceIndex",
                                Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ],
                                [ Ty.path "str" ],
                                "get_unchecked",
                                []
                              |),
                              [ M.read (| self |); M.read (| slice |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut str) -> Option<&mut Self::Output> {
              if self.start <= self.end
                  && slice.is_char_boundary(self.start)
                  && slice.is_char_boundary(self.end)
              {
                  // SAFETY: just checked that `start` and `end` are on a char boundary.
                  // We know the pointer is unique because we got it from `slice`.
                  Some(unsafe { &mut *self.get_unchecked_mut(slice) })
              } else {
                  None
              }
          }
      *)
      Definition get_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            LogicalOp.and (|
                              LogicalOp.and (|
                                BinOp.le (|
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      self,
                                      "core::range::Range",
                                      "start"
                                    |)
                                  |),
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      self,
                                      "core::range::Range",
                                      "end"
                                    |)
                                  |)
                                |),
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "str",
                                      "is_char_boundary",
                                      []
                                    |),
                                    [
                                      M.read (| slice |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          self,
                                          "core::range::Range",
                                          "start"
                                        |)
                                      |)
                                    ]
                                  |)))
                              |),
                              ltac:(M.monadic
                                (M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "str",
                                    "is_char_boundary",
                                    []
                                  |),
                                  [
                                    M.read (| slice |);
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        self,
                                        "core::range::Range",
                                        "end"
                                      |)
                                    |)
                                  ]
                                |)))
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::slice::index::SliceIndex",
                                Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ],
                                [ Ty.path "str" ],
                                "get_unchecked_mut",
                                []
                              |),
                              [ M.read (| self |); M.read (| slice |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const str) -> *const Self::Output {
              let slice = slice as *const [u8];
      
              assert_unsafe_precondition!(
                  // We'd like to check that the bounds are on char boundaries,
                  // but there's not really a way to do so without reading
                  // behind the pointer, which has aliasing implications.
                  // It's also not possible to move this check up to
                  // `str::get_unchecked` without adding a special function
                  // to `SliceIndex` just for this.
                  check_library_ub,
                  "str::get_unchecked requires that the range is within the string slice",
                  (
                      start: usize = self.start,
                      end: usize = self.end,
                      len: usize = slice.len()
                  ) => end >= start && end <= len,
              );
      
              // SAFETY: the caller guarantees that `self` is in bounds of `slice`
              // which satisfies all the conditions for `add`.
              unsafe {
                  let new_len = unchecked_sub(self.end, self.start);
                  ptr::slice_from_raw_parts(slice.as_ptr().add(self.start), new_len) as *const str
              }
          }
      *)
      Definition get_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ slice := M.alloc (| M.rust_cast (M.read (| slice |)) |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::ub_checks", [] |),
                                []
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Self,
                                "precondition_check.get_unchecked",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::range::Range",
                                    "start"
                                  |)
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::range::Range",
                                    "end"
                                  |)
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "*const")
                                      []
                                      [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ new_len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::unchecked_sub", [ Ty.path "usize" ] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (| self, "core::range::Range", "end" |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::range::Range",
                          "start"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.rust_cast
                  (M.call_closure (|
                    M.get_function (| "core::ptr::slice_from_raw_parts", [ Ty.path "u8" ] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                          "add",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "*const")
                                []
                                [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                              "as_ptr",
                              []
                            |),
                            [ M.read (| slice |) ]
                          |);
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "core::range::Range",
                              "start"
                            |)
                          |)
                        ]
                      |);
                      M.read (| new_len |)
                    ]
                  |))
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut str) -> *mut Self::Output {
              let slice = slice as *mut [u8];
      
              assert_unsafe_precondition!(
                  check_library_ub,
                  "str::get_unchecked_mut requires that the range is within the string slice",
                  (
                      start: usize = self.start,
                      end: usize = self.end,
                      len: usize = slice.len()
                  ) => end >= start && end <= len,
              );
      
              // SAFETY: see comments for `get_unchecked`.
              unsafe {
                  let new_len = unchecked_sub(self.end, self.start);
                  ptr::slice_from_raw_parts_mut(slice.as_mut_ptr().add(self.start), new_len) as *mut str
              }
          }
      *)
      Definition get_unchecked_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ slice := M.alloc (| M.rust_cast (M.read (| slice |)) |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::intrinsics::ub_checks", [] |),
                                []
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Self,
                                "precondition_check.get_unchecked_mut",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::range::Range",
                                    "start"
                                  |)
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::range::Range",
                                    "end"
                                  |)
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "*mut")
                                      []
                                      [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| slice |) ]
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ new_len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "core::intrinsics::unchecked_sub", [ Ty.path "usize" ] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (| self, "core::range::Range", "end" |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::range::Range",
                          "start"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.rust_cast
                  (M.call_closure (|
                    M.get_function (| "core::ptr::slice_from_raw_parts_mut", [ Ty.path "u8" ] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "*mut") [] [ Ty.path "u8" ],
                          "add",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "*mut")
                                []
                                [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                              "as_mut_ptr",
                              []
                            |),
                            [ M.read (| slice |) ]
                          |);
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "core::range::Range",
                              "start"
                            |)
                          |)
                        ]
                      |);
                      M.read (| new_len |)
                    ]
                  |))
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &str) -> &Self::Output {
              let (start, end) = (self.start, self.end);
              match self.get(slice) {
                  Some(s) => s,
                  None => super::slice_error_fail(slice, start, end),
              }
          }
      *)
      Definition index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  Value.Tuple
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::range::Range",
                          "start"
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (| self, "core::range::Range", "end" |)
                      |)
                    ]
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let start := M.copy (| γ0_0 |) in
                      let end_ := M.copy (| γ0_1 |) in
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::slice::index::SliceIndex",
                              Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ],
                              [ Ty.path "str" ],
                              "get",
                              []
                            |),
                            [ M.read (| self |); M.read (| slice |) ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let s := M.copy (| γ0_0 |) in
                              M.alloc (| M.read (| s |) |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.call_closure (|
                                    M.get_function (| "core::str::slice_error_fail", [] |),
                                    [ M.read (| slice |); M.read (| start |); M.read (| end_ |) ]
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut str) -> &mut Self::Output {
              // is_char_boundary checks that the index is in [0, .len()]
              // cannot reuse `get` as above, because of NLL trouble
              if self.start <= self.end
                  && slice.is_char_boundary(self.start)
                  && slice.is_char_boundary(self.end)
              {
                  // SAFETY: just checked that `start` and `end` are on a char boundary,
                  // and we are passing in a safe reference, so the return value will also be one.
                  unsafe { &mut *self.get_unchecked_mut(slice) }
              } else {
                  super::slice_error_fail(slice, self.start, self.end)
              }
          }
      *)
      Definition index_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            LogicalOp.and (|
                              LogicalOp.and (|
                                BinOp.le (|
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      self,
                                      "core::range::Range",
                                      "start"
                                    |)
                                  |),
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      self,
                                      "core::range::Range",
                                      "end"
                                    |)
                                  |)
                                |),
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "str",
                                      "is_char_boundary",
                                      []
                                    |),
                                    [
                                      M.read (| slice |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          self,
                                          "core::range::Range",
                                          "start"
                                        |)
                                      |)
                                    ]
                                  |)))
                              |),
                              ltac:(M.monadic
                                (M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "str",
                                    "is_char_boundary",
                                    []
                                  |),
                                  [
                                    M.read (| slice |);
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        self,
                                        "core::range::Range",
                                        "end"
                                      |)
                                    |)
                                  ]
                                |)))
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::slice::index::SliceIndex",
                            Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ],
                            [ Ty.path "str" ],
                            "get_unchecked_mut",
                            []
                          |),
                          [ M.read (| self |); M.read (| slice |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::str::slice_error_fail", [] |),
                            [
                              M.read (| slice |);
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::range::Range",
                                  "start"
                                |)
                              |);
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::range::Range",
                                  "end"
                                |)
                              |)
                            ]
                          |)
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "str" ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty _Output);
            ("get", InstanceField.Method get);
            ("get_mut", InstanceField.Method get_mut);
            ("get_unchecked", InstanceField.Method get_unchecked);
            ("get_unchecked_mut", InstanceField.Method get_unchecked_mut);
            ("index", InstanceField.Method index);
            ("index_mut", InstanceField.Method index_mut)
          ].
    End Impl_core_slice_index_SliceIndex_str_for_core_range_Range_usize.
    
    Module Impl_core_slice_index_SliceIndex_str_for_Tuple_core_ops_range_Bound_usize_core_ops_range_Bound_usize_.
      Definition Self : Ty.t :=
        Ty.tuple
          [
            Ty.apply (Ty.path "core::ops::range::Bound") [] [ Ty.path "usize" ];
            Ty.apply (Ty.path "core::ops::range::Bound") [] [ Ty.path "usize" ]
          ].
      
      (*     type Output = str; *)
      Definition _Output : Ty.t := Ty.path "str".
      
      (*
          fn get(self, slice: &str) -> Option<&str> {
              crate::slice::index::into_range(slice.len(), self)?.get(slice)
          }
      *)
      Definition get (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.path "str" ],
                    "get",
                    []
                  |),
                  [
                    M.read (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply
                                (Ty.path "core::option::Option")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ]
                                ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_function (| "core::slice::index::into_range", [] |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (| Ty.path "str", "len", [] |),
                                    [ M.read (| slice |) ]
                                  |);
                                  M.read (| self |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Break",
                                  0
                                |) in
                              let residual := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::try_trait::FromResidual",
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "from_residual",
                                          []
                                        |),
                                        [ M.read (| residual |) ]
                                      |)
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Continue",
                                  0
                                |) in
                              let val := M.copy (| γ0_0 |) in
                              val))
                        ]
                      |)
                    |);
                    M.read (| slice |)
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut str) -> Option<&mut str> {
              crate::slice::index::into_range(slice.len(), self)?.get_mut(slice)
          }
      *)
      Definition get_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.path "str" ],
                    "get_mut",
                    []
                  |),
                  [
                    M.read (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply
                                (Ty.path "core::option::Option")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::ops::range::Range")
                                    []
                                    [ Ty.path "usize" ]
                                ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_function (| "core::slice::index::into_range", [] |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (| Ty.path "str", "len", [] |),
                                    [ M.read (| slice |) ]
                                  |);
                                  M.read (| self |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Break",
                                  0
                                |) in
                              let residual := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::try_trait::FromResidual",
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.apply (Ty.path "&mut") [] [ Ty.path "str" ] ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::convert::Infallible" ]
                                          ],
                                          "from_residual",
                                          []
                                        |),
                                        [ M.read (| residual |) ]
                                      |)
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Continue",
                                  0
                                |) in
                              let val := M.copy (| γ0_0 |) in
                              val))
                        ]
                      |)
                    |);
                    M.read (| slice |)
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const str) -> *const str {
              let len = (slice as *const [u8]).len();
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked`.
              unsafe { crate::slice::index::into_range_unchecked(len, self).get_unchecked(slice) }
          }
      *)
      Definition get_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "*const")
                        []
                        [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                      "len",
                      []
                    |),
                    [ M.rust_cast (M.read (| slice |)) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.path "str" ],
                    "get_unchecked",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_function (| "core::slice::index::into_range_unchecked", [] |),
                      [ M.read (| len |); M.read (| self |) ]
                    |);
                    M.read (| slice |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut str) -> *mut str {
              let len = (slice as *mut [u8]).len();
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked_mut`.
              unsafe { crate::slice::index::into_range_unchecked(len, self).get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "*mut")
                        []
                        [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                      "len",
                      []
                    |),
                    [ M.rust_cast (M.read (| slice |)) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.path "str" ],
                    "get_unchecked_mut",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_function (| "core::slice::index::into_range_unchecked", [] |),
                      [ M.read (| len |); M.read (| self |) ]
                    |);
                    M.read (| slice |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &str) -> &str {
              crate::slice::index::into_slice_range(slice.len(), self).index(slice)
          }
      *)
      Definition index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.path "str" ],
                "index",
                []
              |),
              [
                M.call_closure (|
                  M.get_function (| "core::slice::index::into_slice_range", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "str", "len", [] |),
                      [ M.read (| slice |) ]
                    |);
                    M.read (| self |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut str) -> &mut str {
              crate::slice::index::into_slice_range(slice.len(), self).index_mut(slice)
          }
      *)
      Definition index_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.path "str" ],
                "index_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_function (| "core::slice::index::into_slice_range", [] |),
                  [
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "str", "len", [] |),
                      [ M.read (| slice |) ]
                    |);
                    M.read (| self |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "str" ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty _Output);
            ("get", InstanceField.Method get);
            ("get_mut", InstanceField.Method get_mut);
            ("get_unchecked", InstanceField.Method get_unchecked);
            ("get_unchecked_mut", InstanceField.Method get_unchecked_mut);
            ("index", InstanceField.Method index);
            ("index_mut", InstanceField.Method index_mut)
          ].
    End Impl_core_slice_index_SliceIndex_str_for_Tuple_core_ops_range_Bound_usize_core_ops_range_Bound_usize_.
    
    Module Impl_core_slice_index_SliceIndex_str_for_core_ops_range_RangeTo_usize.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ].
      
      (*     type Output = str; *)
      Definition _Output : Ty.t := Ty.path "str".
      
      (*
          fn get(self, slice: &str) -> Option<&Self::Output> {
              if slice.is_char_boundary(self.end) {
                  // SAFETY: just checked that `end` is on a char boundary,
                  // and we are passing in a safe reference, so the return value will also be one.
                  Some(unsafe { &*self.get_unchecked(slice) })
              } else {
                  None
              }
          }
      *)
      Definition get (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "str", "is_char_boundary", [] |),
                              [
                                M.read (| slice |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::RangeTo",
                                    "end"
                                  |)
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::slice::index::SliceIndex",
                                Ty.apply
                                  (Ty.path "core::ops::range::RangeTo")
                                  []
                                  [ Ty.path "usize" ],
                                [ Ty.path "str" ],
                                "get_unchecked",
                                []
                              |),
                              [ M.read (| self |); M.read (| slice |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut str) -> Option<&mut Self::Output> {
              if slice.is_char_boundary(self.end) {
                  // SAFETY: just checked that `end` is on a char boundary,
                  // and we are passing in a safe reference, so the return value will also be one.
                  Some(unsafe { &mut *self.get_unchecked_mut(slice) })
              } else {
                  None
              }
          }
      *)
      Definition get_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "str", "is_char_boundary", [] |),
                              [
                                M.read (| slice |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::RangeTo",
                                    "end"
                                  |)
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::slice::index::SliceIndex",
                                Ty.apply
                                  (Ty.path "core::ops::range::RangeTo")
                                  []
                                  [ Ty.path "usize" ],
                                [ Ty.path "str" ],
                                "get_unchecked_mut",
                                []
                              |),
                              [ M.read (| self |); M.read (| slice |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const str) -> *const Self::Output {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked`.
              unsafe { (0..self.end).get_unchecked(slice) }
          }
      *)
      Definition get_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.path "str" ],
                "get_unchecked",
                []
              |),
              [
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start", Value.Integer IntegerKind.Usize 0);
                    ("end_",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::RangeTo",
                          "end"
                        |)
                      |))
                  ];
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut str) -> *mut Self::Output {
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked_mut`.
              unsafe { (0..self.end).get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.path "str" ],
                "get_unchecked_mut",
                []
              |),
              [
                Value.StructRecord
                  "core::ops::range::Range"
                  [
                    ("start", Value.Integer IntegerKind.Usize 0);
                    ("end_",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::RangeTo",
                          "end"
                        |)
                      |))
                  ];
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &str) -> &Self::Output {
              let end = self.end;
              match self.get(slice) {
                  Some(s) => s,
                  None => super::slice_error_fail(slice, 0, end),
              }
          }
      *)
      Definition index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ end_ :=
                M.copy (|
                  M.SubPointer.get_struct_record_field (|
                    self,
                    "core::ops::range::RangeTo",
                    "end"
                  |)
                |) in
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::slice::index::SliceIndex",
                      Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ],
                      [ Ty.path "str" ],
                      "get",
                      []
                    |),
                    [ M.read (| self |); M.read (| slice |) ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let s := M.copy (| γ0_0 |) in
                      M.alloc (| M.read (| s |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::str::slice_error_fail", [] |),
                            [
                              M.read (| slice |);
                              Value.Integer IntegerKind.Usize 0;
                              M.read (| end_ |)
                            ]
                          |)
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut str) -> &mut Self::Output {
              if slice.is_char_boundary(self.end) {
                  // SAFETY: just checked that `end` is on a char boundary,
                  // and we are passing in a safe reference, so the return value will also be one.
                  unsafe { &mut *self.get_unchecked_mut(slice) }
              } else {
                  super::slice_error_fail(slice, 0, self.end)
              }
          }
      *)
      Definition index_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "str", "is_char_boundary", [] |),
                              [
                                M.read (| slice |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::RangeTo",
                                    "end"
                                  |)
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::slice::index::SliceIndex",
                            Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ],
                            [ Ty.path "str" ],
                            "get_unchecked_mut",
                            []
                          |),
                          [ M.read (| self |); M.read (| slice |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::str::slice_error_fail", [] |),
                            [
                              M.read (| slice |);
                              Value.Integer IntegerKind.Usize 0;
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::ops::range::RangeTo",
                                  "end"
                                |)
                              |)
                            ]
                          |)
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "str" ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty _Output);
            ("get", InstanceField.Method get);
            ("get_mut", InstanceField.Method get_mut);
            ("get_unchecked", InstanceField.Method get_unchecked);
            ("get_unchecked_mut", InstanceField.Method get_unchecked_mut);
            ("index", InstanceField.Method index);
            ("index_mut", InstanceField.Method index_mut)
          ].
    End Impl_core_slice_index_SliceIndex_str_for_core_ops_range_RangeTo_usize.
    
    Module Impl_core_slice_index_SliceIndex_str_for_core_ops_range_RangeFrom_usize.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ].
      
      (*     type Output = str; *)
      Definition _Output : Ty.t := Ty.path "str".
      
      (*
          fn get(self, slice: &str) -> Option<&Self::Output> {
              if slice.is_char_boundary(self.start) {
                  // SAFETY: just checked that `start` is on a char boundary,
                  // and we are passing in a safe reference, so the return value will also be one.
                  Some(unsafe { &*self.get_unchecked(slice) })
              } else {
                  None
              }
          }
      *)
      Definition get (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "str", "is_char_boundary", [] |),
                              [
                                M.read (| slice |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::RangeFrom",
                                    "start"
                                  |)
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::slice::index::SliceIndex",
                                Ty.apply
                                  (Ty.path "core::ops::range::RangeFrom")
                                  []
                                  [ Ty.path "usize" ],
                                [ Ty.path "str" ],
                                "get_unchecked",
                                []
                              |),
                              [ M.read (| self |); M.read (| slice |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut str) -> Option<&mut Self::Output> {
              if slice.is_char_boundary(self.start) {
                  // SAFETY: just checked that `start` is on a char boundary,
                  // and we are passing in a safe reference, so the return value will also be one.
                  Some(unsafe { &mut *self.get_unchecked_mut(slice) })
              } else {
                  None
              }
          }
      *)
      Definition get_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "str", "is_char_boundary", [] |),
                              [
                                M.read (| slice |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::RangeFrom",
                                    "start"
                                  |)
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::slice::index::SliceIndex",
                                Ty.apply
                                  (Ty.path "core::ops::range::RangeFrom")
                                  []
                                  [ Ty.path "usize" ],
                                [ Ty.path "str" ],
                                "get_unchecked_mut",
                                []
                              |),
                              [ M.read (| self |); M.read (| slice |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const str) -> *const Self::Output {
              let len = (slice as *const [u8]).len();
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked`.
              unsafe { (self.start..len).get_unchecked(slice) }
          }
      *)
      Definition get_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "*const")
                        []
                        [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                      "len",
                      []
                    |),
                    [ M.rust_cast (M.read (| slice |)) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.path "str" ],
                    "get_unchecked",
                    []
                  |),
                  [
                    Value.StructRecord
                      "core::ops::range::Range"
                      [
                        ("start",
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "core::ops::range::RangeFrom",
                              "start"
                            |)
                          |));
                        ("end_", M.read (| len |))
                      ];
                    M.read (| slice |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut str) -> *mut Self::Output {
              let len = (slice as *mut [u8]).len();
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked_mut`.
              unsafe { (self.start..len).get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "*mut")
                        []
                        [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                      "len",
                      []
                    |),
                    [ M.rust_cast (M.read (| slice |)) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.path "str" ],
                    "get_unchecked_mut",
                    []
                  |),
                  [
                    Value.StructRecord
                      "core::ops::range::Range"
                      [
                        ("start",
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "core::ops::range::RangeFrom",
                              "start"
                            |)
                          |));
                        ("end_", M.read (| len |))
                      ];
                    M.read (| slice |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &str) -> &Self::Output {
              let (start, end) = (self.start, slice.len());
              match self.get(slice) {
                  Some(s) => s,
                  None => super::slice_error_fail(slice, start, end),
              }
          }
      *)
      Definition index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  Value.Tuple
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::ops::range::RangeFrom",
                          "start"
                        |)
                      |);
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "str", "len", [] |),
                        [ M.read (| slice |) ]
                      |)
                    ]
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let start := M.copy (| γ0_0 |) in
                      let end_ := M.copy (| γ0_1 |) in
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::slice::index::SliceIndex",
                              Ty.apply
                                (Ty.path "core::ops::range::RangeFrom")
                                []
                                [ Ty.path "usize" ],
                              [ Ty.path "str" ],
                              "get",
                              []
                            |),
                            [ M.read (| self |); M.read (| slice |) ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let s := M.copy (| γ0_0 |) in
                              M.alloc (| M.read (| s |) |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.call_closure (|
                                    M.get_function (| "core::str::slice_error_fail", [] |),
                                    [ M.read (| slice |); M.read (| start |); M.read (| end_ |) ]
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut str) -> &mut Self::Output {
              if slice.is_char_boundary(self.start) {
                  // SAFETY: just checked that `start` is on a char boundary,
                  // and we are passing in a safe reference, so the return value will also be one.
                  unsafe { &mut *self.get_unchecked_mut(slice) }
              } else {
                  super::slice_error_fail(slice, self.start, slice.len())
              }
          }
      *)
      Definition index_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "str", "is_char_boundary", [] |),
                              [
                                M.read (| slice |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::ops::range::RangeFrom",
                                    "start"
                                  |)
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::slice::index::SliceIndex",
                            Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ],
                            [ Ty.path "str" ],
                            "get_unchecked_mut",
                            []
                          |),
                          [ M.read (| self |); M.read (| slice |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::str::slice_error_fail", [] |),
                            [
                              M.read (| slice |);
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::ops::range::RangeFrom",
                                  "start"
                                |)
                              |);
                              M.call_closure (|
                                M.get_associated_function (| Ty.path "str", "len", [] |),
                                [ M.read (| slice |) ]
                              |)
                            ]
                          |)
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "str" ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty _Output);
            ("get", InstanceField.Method get);
            ("get_mut", InstanceField.Method get_mut);
            ("get_unchecked", InstanceField.Method get_unchecked);
            ("get_unchecked_mut", InstanceField.Method get_unchecked_mut);
            ("index", InstanceField.Method index);
            ("index_mut", InstanceField.Method index_mut)
          ].
    End Impl_core_slice_index_SliceIndex_str_for_core_ops_range_RangeFrom_usize.
    
    Module Impl_core_slice_index_SliceIndex_str_for_core_range_RangeFrom_usize.
      Definition Self : Ty.t := Ty.apply (Ty.path "core::range::RangeFrom") [] [ Ty.path "usize" ].
      
      (*     type Output = str; *)
      Definition _Output : Ty.t := Ty.path "str".
      
      (*
          fn get(self, slice: &str) -> Option<&Self::Output> {
              if slice.is_char_boundary(self.start) {
                  // SAFETY: just checked that `start` is on a char boundary,
                  // and we are passing in a safe reference, so the return value will also be one.
                  Some(unsafe { &*self.get_unchecked(slice) })
              } else {
                  None
              }
          }
      *)
      Definition get (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "str", "is_char_boundary", [] |),
                              [
                                M.read (| slice |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::range::RangeFrom",
                                    "start"
                                  |)
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::slice::index::SliceIndex",
                                Ty.apply (Ty.path "core::range::RangeFrom") [] [ Ty.path "usize" ],
                                [ Ty.path "str" ],
                                "get_unchecked",
                                []
                              |),
                              [ M.read (| self |); M.read (| slice |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut str) -> Option<&mut Self::Output> {
              if slice.is_char_boundary(self.start) {
                  // SAFETY: just checked that `start` is on a char boundary,
                  // and we are passing in a safe reference, so the return value will also be one.
                  Some(unsafe { &mut *self.get_unchecked_mut(slice) })
              } else {
                  None
              }
          }
      *)
      Definition get_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "str", "is_char_boundary", [] |),
                              [
                                M.read (| slice |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::range::RangeFrom",
                                    "start"
                                  |)
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::slice::index::SliceIndex",
                                Ty.apply (Ty.path "core::range::RangeFrom") [] [ Ty.path "usize" ],
                                [ Ty.path "str" ],
                                "get_unchecked_mut",
                                []
                              |),
                              [ M.read (| self |); M.read (| slice |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const str) -> *const Self::Output {
              let len = (slice as *const [u8]).len();
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked`.
              unsafe { (self.start..len).get_unchecked(slice) }
          }
      *)
      Definition get_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "*const")
                        []
                        [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                      "len",
                      []
                    |),
                    [ M.rust_cast (M.read (| slice |)) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.path "str" ],
                    "get_unchecked",
                    []
                  |),
                  [
                    Value.StructRecord
                      "core::ops::range::Range"
                      [
                        ("start",
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "core::range::RangeFrom",
                              "start"
                            |)
                          |));
                        ("end_", M.read (| len |))
                      ];
                    M.read (| slice |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut str) -> *mut Self::Output {
              let len = (slice as *mut [u8]).len();
              // SAFETY: the caller has to uphold the safety contract for `get_unchecked_mut`.
              unsafe { (self.start..len).get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "*mut")
                        []
                        [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                      "len",
                      []
                    |),
                    [ M.rust_cast (M.read (| slice |)) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.path "str" ],
                    "get_unchecked_mut",
                    []
                  |),
                  [
                    Value.StructRecord
                      "core::ops::range::Range"
                      [
                        ("start",
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              self,
                              "core::range::RangeFrom",
                              "start"
                            |)
                          |));
                        ("end_", M.read (| len |))
                      ];
                    M.read (| slice |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &str) -> &Self::Output {
              let (start, end) = (self.start, slice.len());
              match self.get(slice) {
                  Some(s) => s,
                  None => super::slice_error_fail(slice, start, end),
              }
          }
      *)
      Definition index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  Value.Tuple
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "core::range::RangeFrom",
                          "start"
                        |)
                      |);
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "str", "len", [] |),
                        [ M.read (| slice |) ]
                      |)
                    ]
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let start := M.copy (| γ0_0 |) in
                      let end_ := M.copy (| γ0_1 |) in
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::slice::index::SliceIndex",
                              Ty.apply (Ty.path "core::range::RangeFrom") [] [ Ty.path "usize" ],
                              [ Ty.path "str" ],
                              "get",
                              []
                            |),
                            [ M.read (| self |); M.read (| slice |) ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let s := M.copy (| γ0_0 |) in
                              M.alloc (| M.read (| s |) |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.call_closure (|
                                    M.get_function (| "core::str::slice_error_fail", [] |),
                                    [ M.read (| slice |); M.read (| start |); M.read (| end_ |) ]
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut str) -> &mut Self::Output {
              if slice.is_char_boundary(self.start) {
                  // SAFETY: just checked that `start` is on a char boundary,
                  // and we are passing in a safe reference, so the return value will also be one.
                  unsafe { &mut *self.get_unchecked_mut(slice) }
              } else {
                  super::slice_error_fail(slice, self.start, slice.len())
              }
          }
      *)
      Definition index_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "str", "is_char_boundary", [] |),
                              [
                                M.read (| slice |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::range::RangeFrom",
                                    "start"
                                  |)
                                |)
                              ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::slice::index::SliceIndex",
                            Ty.apply (Ty.path "core::range::RangeFrom") [] [ Ty.path "usize" ],
                            [ Ty.path "str" ],
                            "get_unchecked_mut",
                            []
                          |),
                          [ M.read (| self |); M.read (| slice |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::str::slice_error_fail", [] |),
                            [
                              M.read (| slice |);
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::range::RangeFrom",
                                  "start"
                                |)
                              |);
                              M.call_closure (|
                                M.get_associated_function (| Ty.path "str", "len", [] |),
                                [ M.read (| slice |) ]
                              |)
                            ]
                          |)
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "str" ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty _Output);
            ("get", InstanceField.Method get);
            ("get_mut", InstanceField.Method get_mut);
            ("get_unchecked", InstanceField.Method get_unchecked);
            ("get_unchecked_mut", InstanceField.Method get_unchecked_mut);
            ("index", InstanceField.Method index);
            ("index_mut", InstanceField.Method index_mut)
          ].
    End Impl_core_slice_index_SliceIndex_str_for_core_range_RangeFrom_usize.
    
    Module Impl_core_slice_index_SliceIndex_str_for_core_ops_range_RangeInclusive_usize.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ].
      
      (*     type Output = str; *)
      Definition _Output : Ty.t := Ty.path "str".
      
      (*
          fn get(self, slice: &str) -> Option<&Self::Output> {
              if *self.end() == usize::MAX { None } else { self.into_slice_range().get(slice) }
          }
      *)
      Definition get (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.eq (|
                              M.read (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::ops::range::RangeInclusive")
                                      []
                                      [ Ty.path "usize" ],
                                    "end",
                                    []
                                  |),
                                  [ self ]
                                |)
                              |),
                              M.read (| M.get_constant (| "core::num::MAX" |) |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::slice::index::SliceIndex",
                            Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                            [ Ty.path "str" ],
                            "get",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::ops::range::RangeInclusive")
                                  []
                                  [ Ty.path "usize" ],
                                "into_slice_range",
                                []
                              |),
                              [ M.read (| self |) ]
                            |);
                            M.read (| slice |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut str) -> Option<&mut Self::Output> {
              if *self.end() == usize::MAX { None } else { self.into_slice_range().get_mut(slice) }
          }
      *)
      Definition get_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.eq (|
                              M.read (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::ops::range::RangeInclusive")
                                      []
                                      [ Ty.path "usize" ],
                                    "end",
                                    []
                                  |),
                                  [ self ]
                                |)
                              |),
                              M.read (| M.get_constant (| "core::num::MAX" |) |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::slice::index::SliceIndex",
                            Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                            [ Ty.path "str" ],
                            "get_mut",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::ops::range::RangeInclusive")
                                  []
                                  [ Ty.path "usize" ],
                                "into_slice_range",
                                []
                              |),
                              [ M.read (| self |) ]
                            |);
                            M.read (| slice |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const str) -> *const Self::Output {
              // SAFETY: the caller must uphold the safety contract for `get_unchecked`.
              unsafe { self.into_slice_range().get_unchecked(slice) }
          }
      *)
      Definition get_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.path "str" ],
                "get_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "into_slice_range",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut str) -> *mut Self::Output {
              // SAFETY: the caller must uphold the safety contract for `get_unchecked_mut`.
              unsafe { self.into_slice_range().get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                [ Ty.path "str" ],
                "get_unchecked_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "into_slice_range",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &str) -> &Self::Output {
              if *self.end() == usize::MAX {
                  str_index_overflow_fail();
              }
              self.into_slice_range().index(slice)
          }
      *)
      Definition index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.eq (|
                                M.read (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::ops::range::RangeInclusive")
                                        []
                                        [ Ty.path "usize" ],
                                      "end",
                                      []
                                    |),
                                    [ self ]
                                  |)
                                |),
                                M.read (| M.get_constant (| "core::num::MAX" |) |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::str::traits::str_index_overflow_fail", [] |),
                              []
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.path "str" ],
                    "index",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::ops::range::RangeInclusive")
                          []
                          [ Ty.path "usize" ],
                        "into_slice_range",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| slice |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut str) -> &mut Self::Output {
              if *self.end() == usize::MAX {
                  str_index_overflow_fail();
              }
              self.into_slice_range().index_mut(slice)
          }
      *)
      Definition index_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.eq (|
                                M.read (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::ops::range::RangeInclusive")
                                        []
                                        [ Ty.path "usize" ],
                                      "end",
                                      []
                                    |),
                                    [ self ]
                                  |)
                                |),
                                M.read (| M.get_constant (| "core::num::MAX" |) |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::str::traits::str_index_overflow_fail", [] |),
                              []
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.path "str" ],
                    "index_mut",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::ops::range::RangeInclusive")
                          []
                          [ Ty.path "usize" ],
                        "into_slice_range",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| slice |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "str" ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty _Output);
            ("get", InstanceField.Method get);
            ("get_mut", InstanceField.Method get_mut);
            ("get_unchecked", InstanceField.Method get_unchecked);
            ("get_unchecked_mut", InstanceField.Method get_unchecked_mut);
            ("index", InstanceField.Method index);
            ("index_mut", InstanceField.Method index_mut)
          ].
    End Impl_core_slice_index_SliceIndex_str_for_core_ops_range_RangeInclusive_usize.
    
    Module Impl_core_slice_index_SliceIndex_str_for_core_range_RangeInclusive_usize.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.path "usize" ].
      
      (*     type Output = str; *)
      Definition _Output : Ty.t := Ty.path "str".
      
      (*
          fn get(self, slice: &str) -> Option<&Self::Output> {
              if self.end == usize::MAX { None } else { self.into_slice_range().get(slice) }
          }
      *)
      Definition get (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.eq (|
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::range::RangeInclusive",
                                  "end"
                                |)
                              |),
                              M.read (| M.get_constant (| "core::num::MAX" |) |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::slice::index::SliceIndex",
                            Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ],
                            [ Ty.path "str" ],
                            "get",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::range::RangeInclusive")
                                  []
                                  [ Ty.path "usize" ],
                                "into_slice_range",
                                []
                              |),
                              [ M.read (| self |) ]
                            |);
                            M.read (| slice |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut str) -> Option<&mut Self::Output> {
              if self.end == usize::MAX { None } else { self.into_slice_range().get_mut(slice) }
          }
      *)
      Definition get_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.eq (|
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "core::range::RangeInclusive",
                                  "end"
                                |)
                              |),
                              M.read (| M.get_constant (| "core::num::MAX" |) |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::slice::index::SliceIndex",
                            Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ],
                            [ Ty.path "str" ],
                            "get_mut",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::range::RangeInclusive")
                                  []
                                  [ Ty.path "usize" ],
                                "into_slice_range",
                                []
                              |),
                              [ M.read (| self |) ]
                            |);
                            M.read (| slice |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const str) -> *const Self::Output {
              // SAFETY: the caller must uphold the safety contract for `get_unchecked`.
              unsafe { self.into_slice_range().get_unchecked(slice) }
          }
      *)
      Definition get_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ],
                [ Ty.path "str" ],
                "get_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "into_slice_range",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut str) -> *mut Self::Output {
              // SAFETY: the caller must uphold the safety contract for `get_unchecked_mut`.
              unsafe { self.into_slice_range().get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ],
                [ Ty.path "str" ],
                "get_unchecked_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "into_slice_range",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &str) -> &Self::Output {
              if self.end == usize::MAX {
                  str_index_overflow_fail();
              }
              self.into_slice_range().index(slice)
          }
      *)
      Definition index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.eq (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::range::RangeInclusive",
                                    "end"
                                  |)
                                |),
                                M.read (| M.get_constant (| "core::num::MAX" |) |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::str::traits::str_index_overflow_fail", [] |),
                              []
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.path "str" ],
                    "index",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.path "usize" ],
                        "into_slice_range",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| slice |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut str) -> &mut Self::Output {
              if self.end == usize::MAX {
                  str_index_overflow_fail();
              }
              self.into_slice_range().index_mut(slice)
          }
      *)
      Definition index_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.eq (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "core::range::RangeInclusive",
                                    "end"
                                  |)
                                |),
                                M.read (| M.get_constant (| "core::num::MAX" |) |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::str::traits::str_index_overflow_fail", [] |),
                              []
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::slice::index::SliceIndex",
                    Ty.apply (Ty.path "core::range::Range") [] [ Ty.path "usize" ],
                    [ Ty.path "str" ],
                    "index_mut",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::range::RangeInclusive") [] [ Ty.path "usize" ],
                        "into_slice_range",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| slice |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "str" ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty _Output);
            ("get", InstanceField.Method get);
            ("get_mut", InstanceField.Method get_mut);
            ("get_unchecked", InstanceField.Method get_unchecked);
            ("get_unchecked_mut", InstanceField.Method get_unchecked_mut);
            ("index", InstanceField.Method index);
            ("index_mut", InstanceField.Method index_mut)
          ].
    End Impl_core_slice_index_SliceIndex_str_for_core_range_RangeInclusive_usize.
    
    Module Impl_core_slice_index_SliceIndex_str_for_core_ops_range_RangeToInclusive_usize.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "core::ops::range::RangeToInclusive") [] [ Ty.path "usize" ].
      
      (*     type Output = str; *)
      Definition _Output : Ty.t := Ty.path "str".
      
      (*
          fn get(self, slice: &str) -> Option<&Self::Output> {
              (0..=self.end).get(slice)
          }
      *)
      Definition get (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.path "str" ],
                "get",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "new",
                    []
                  |),
                  [
                    Value.Integer IntegerKind.Usize 0;
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ops::range::RangeToInclusive",
                        "end"
                      |)
                    |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn get_mut(self, slice: &mut str) -> Option<&mut Self::Output> {
              (0..=self.end).get_mut(slice)
          }
      *)
      Definition get_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.path "str" ],
                "get_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "new",
                    []
                  |),
                  [
                    Value.Integer IntegerKind.Usize 0;
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ops::range::RangeToInclusive",
                        "end"
                      |)
                    |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked(self, slice: *const str) -> *const Self::Output {
              // SAFETY: the caller must uphold the safety contract for `get_unchecked`.
              unsafe { (0..=self.end).get_unchecked(slice) }
          }
      *)
      Definition get_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.path "str" ],
                "get_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "new",
                    []
                  |),
                  [
                    Value.Integer IntegerKind.Usize 0;
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ops::range::RangeToInclusive",
                        "end"
                      |)
                    |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          unsafe fn get_unchecked_mut(self, slice: *mut str) -> *mut Self::Output {
              // SAFETY: the caller must uphold the safety contract for `get_unchecked_mut`.
              unsafe { (0..=self.end).get_unchecked_mut(slice) }
          }
      *)
      Definition get_unchecked_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.path "str" ],
                "get_unchecked_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "new",
                    []
                  |),
                  [
                    Value.Integer IntegerKind.Usize 0;
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ops::range::RangeToInclusive",
                        "end"
                      |)
                    |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index(self, slice: &str) -> &Self::Output {
              (0..=self.end).index(slice)
          }
      *)
      Definition index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.path "str" ],
                "index",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "new",
                    []
                  |),
                  [
                    Value.Integer IntegerKind.Usize 0;
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ops::range::RangeToInclusive",
                        "end"
                      |)
                    |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn index_mut(self, slice: &mut str) -> &mut Self::Output {
              (0..=self.end).index_mut(slice)
          }
      *)
      Definition index_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::slice::index::SliceIndex",
                Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                [ Ty.path "str" ],
                "index_mut",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "usize" ],
                    "new",
                    []
                  |),
                  [
                    Value.Integer IntegerKind.Usize 0;
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "core::ops::range::RangeToInclusive",
                        "end"
                      |)
                    |)
                  ]
                |);
                M.read (| slice |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::slice::index::SliceIndex"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "str" ]
          (* Instance *)
          [
            ("Output", InstanceField.Ty _Output);
            ("get", InstanceField.Method get);
            ("get_mut", InstanceField.Method get_mut);
            ("get_unchecked", InstanceField.Method get_unchecked);
            ("get_unchecked_mut", InstanceField.Method get_unchecked_mut);
            ("index", InstanceField.Method index);
            ("index_mut", InstanceField.Method index_mut)
          ].
    End Impl_core_slice_index_SliceIndex_str_for_core_ops_range_RangeToInclusive_usize.
    
    (* Trait *)
    (* Empty module 'FromStr' *)
    
    Module Impl_core_str_traits_FromStr_for_bool.
      Definition Self : Ty.t := Ty.path "bool".
      
      (*     type Err = ParseBoolError; *)
      Definition _Err : Ty.t := Ty.path "core::str::error::ParseBoolError".
      
      (*
          fn from_str(s: &str) -> Result<bool, ParseBoolError> {
              match s {
                  "true" => Ok(true),
                  "false" => Ok(false),
                  _ => Err(ParseBoolError),
              }
          }
      *)
      Definition from_str (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            M.read (|
              M.match_operator (|
                s,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (| M.read (| γ |), Value.String "true" |) in
                      M.alloc (|
                        Value.StructTuple "core::result::Result::Ok" [ Value.Bool true ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (| M.read (| γ |), Value.String "false" |) in
                      M.alloc (|
                        Value.StructTuple "core::result::Result::Ok" [ Value.Bool false ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [ Value.StructTuple "core::str::error::ParseBoolError" [] ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::str::traits::FromStr"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Err", InstanceField.Ty _Err); ("from_str", InstanceField.Method from_str) ].
    End Impl_core_str_traits_FromStr_for_bool.
  End traits.
End str.
