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

Module ops.
  Module index_range.
    (* StructRecord
      {
        name := "IndexRange";
        const_params := [];
        ty_params := [];
        fields := [ ("start", Ty.path "usize"); ("end_", Ty.path "usize") ];
      } *)
    
    Module Impl_core_clone_Clone_for_core_ops_index_range_IndexRange.
      Definition Self : Ty.t := Ty.path "core::ops::index_range::IndexRange".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "core::ops::index_range::IndexRange"
              [
                ("start",
                  M.call_closure (|
                    M.get_trait_method (| "core::clone::Clone", Ty.path "usize", [], "clone", [] |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::ops::index_range::IndexRange",
                        "start"
                      |)
                    ]
                  |));
                ("end_",
                  M.call_closure (|
                    M.get_trait_method (| "core::clone::Clone", Ty.path "usize", [], "clone", [] |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::ops::index_range::IndexRange",
                        "end"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_ops_index_range_IndexRange.
    
    Module Impl_core_fmt_Debug_for_core_ops_index_range_IndexRange.
      Definition Self : Ty.t := Ty.path "core::ops::index_range::IndexRange".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_struct_field2_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "IndexRange" |);
                M.read (| Value.String "start" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::ops::index_range::IndexRange",
                  "start"
                |);
                M.read (| Value.String "end" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::ops::index_range::IndexRange",
                    "end"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_ops_index_range_IndexRange.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_ops_index_range_IndexRange.
      Definition Self : Ty.t := Ty.path "core::ops::index_range::IndexRange".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_ops_index_range_IndexRange.
    
    Module Impl_core_cmp_PartialEq_for_core_ops_index_range_IndexRange.
      Definition Self : Ty.t := Ty.path "core::ops::index_range::IndexRange".
      
      (* PartialEq *)
      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
            LogicalOp.and (|
              BinOp.eq (|
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::ops::index_range::IndexRange",
                    "start"
                  |)
                |),
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "core::ops::index_range::IndexRange",
                    "start"
                  |)
                |)
              |),
              ltac:(M.monadic
                (BinOp.eq (|
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::ops::index_range::IndexRange",
                      "end"
                    |)
                  |),
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "core::ops::index_range::IndexRange",
                      "end"
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => 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_core_ops_index_range_IndexRange.
    
    Module Impl_core_cmp_Eq_for_core_ops_index_range_IndexRange.
      Definition Self : Ty.t := Ty.path "core::ops::index_range::IndexRange".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_ops_index_range_IndexRange.
    
    Module Impl_core_ops_index_range_IndexRange.
      Definition Self : Ty.t := Ty.path "core::ops::index_range::IndexRange".
      
      (*
          pub const unsafe fn new_unchecked(start: usize, end: usize) -> Self {
              ub_checks::assert_unsafe_precondition!(
                  check_library_ub,
                  "IndexRange::new_unchecked requires `start <= end`",
                  (start: usize = start, end: usize = end) => start <= end,
              );
              IndexRange { start, end }
          }
      *)
      Definition new_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ start; end_ ] =>
          ltac:(M.monadic
            (let start := M.alloc (| start |) in
            let end_ := M.alloc (| end_ |) in
            M.read (|
              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.new_unchecked",
                                []
                              |),
                              [ M.read (| start |); M.read (| end_ |) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                Value.StructRecord
                  "core::ops::index_range::IndexRange"
                  [ ("start", M.read (| start |)); ("end_", M.read (| end_ |)) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_unchecked :
        M.IsAssociatedFunction Self "new_unchecked" new_unchecked.
      
      (*
          pub const fn zero_to(end: usize) -> Self {
              IndexRange { start: 0, end }
          }
      *)
      Definition zero_to (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ end_ ] =>
          ltac:(M.monadic
            (let end_ := M.alloc (| end_ |) in
            Value.StructRecord
              "core::ops::index_range::IndexRange"
              [ ("start", Value.Integer IntegerKind.Usize 0); ("end_", M.read (| end_ |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_zero_to : M.IsAssociatedFunction Self "zero_to" zero_to.
      
      (*
          pub const fn start(&self) -> usize {
              self.start
          }
      *)
      Definition start (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::ops::index_range::IndexRange",
                "start"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_start : M.IsAssociatedFunction Self "start" start.
      
      (*
          pub const fn end(&self) -> usize {
              self.end
          }
      *)
      Definition end_ (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::ops::index_range::IndexRange",
                "end"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_end_ : M.IsAssociatedFunction Self "end_" end_.
      
      (*
          pub const fn len(&self) -> usize {
              // SAFETY: By invariant, this cannot wrap
              unsafe { self.end.unchecked_sub(self.start) }
          }
      *)
      Definition len (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "usize", "unchecked_sub", [] |),
              [
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::ops::index_range::IndexRange",
                    "end"
                  |)
                |);
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::ops::index_range::IndexRange",
                    "start"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_len : M.IsAssociatedFunction Self "len" len.
      
      (*
          unsafe fn next_unchecked(&mut self) -> usize {
              debug_assert!(self.start < self.end);
      
              let value = self.start;
              // SAFETY: The range isn't empty, so this cannot overflow
              self.start = unsafe { value.unchecked_add(1) };
              value
          }
      *)
      Definition next_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.use (M.alloc (| Value.Bool true |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        UnOp.not (|
                                          BinOp.lt (|
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "core::ops::index_range::IndexRange",
                                                "start"
                                              |)
                                            |),
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "core::ops::index_range::IndexRange",
                                                "end"
                                              |)
                                            |)
                                          |)
                                        |)
                                      |)) 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::panicking::panic", [] |),
                                        [
                                          M.read (|
                                            Value.String "assertion failed: self.start < self.end"
                                          |)
                                        ]
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ value :=
                M.copy (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::ops::index_range::IndexRange",
                    "start"
                  |)
                |) in
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::ops::index_range::IndexRange",
                    "start"
                  |),
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "usize", "unchecked_add", [] |),
                    [ M.read (| value |); Value.Integer IntegerKind.Usize 1 ]
                  |)
                |) in
              value
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_next_unchecked :
        M.IsAssociatedFunction Self "next_unchecked" next_unchecked.
      
      (*
          unsafe fn next_back_unchecked(&mut self) -> usize {
              debug_assert!(self.start < self.end);
      
              // SAFETY: The range isn't empty, so this cannot overflow
              let value = unsafe { self.end.unchecked_sub(1) };
              self.end = value;
              value
          }
      *)
      Definition next_back_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.use (M.alloc (| Value.Bool true |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        UnOp.not (|
                                          BinOp.lt (|
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "core::ops::index_range::IndexRange",
                                                "start"
                                              |)
                                            |),
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "core::ops::index_range::IndexRange",
                                                "end"
                                              |)
                                            |)
                                          |)
                                        |)
                                      |)) 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::panicking::panic", [] |),
                                        [
                                          M.read (|
                                            Value.String "assertion failed: self.start < self.end"
                                          |)
                                        ]
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ value :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "usize", "unchecked_sub", [] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "core::ops::index_range::IndexRange",
                          "end"
                        |)
                      |);
                      Value.Integer IntegerKind.Usize 1
                    ]
                  |)
                |) in
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::ops::index_range::IndexRange",
                    "end"
                  |),
                  M.read (| value |)
                |) in
              value
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_next_back_unchecked :
        M.IsAssociatedFunction Self "next_back_unchecked" next_back_unchecked.
      
      (*
          pub fn take_prefix(&mut self, n: usize) -> Self {
              let mid = if n <= self.len() {
                  // SAFETY: We just checked that this will be between start and end,
                  // and thus the addition cannot overflow.
                  unsafe { self.start.unchecked_add(n) }
              } else {
                  self.end
              };
              let prefix = Self { start: self.start, end: mid };
              self.start = mid;
              prefix
          }
      *)
      Definition take_prefix (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ mid :=
                M.copy (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.le (|
                                  M.read (| n |),
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::exact_size::ExactSizeIterator",
                                      Ty.apply
                                        (Ty.path "&mut")
                                        []
                                        [ Ty.path "core::ops::index_range::IndexRange" ],
                                      [],
                                      "len",
                                      []
                                    |),
                                    [ self ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "usize", "unchecked_add", [] |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::ops::index_range::IndexRange",
                                    "start"
                                  |)
                                |);
                                M.read (| n |)
                              ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::ops::index_range::IndexRange",
                            "end"
                          |)))
                    ]
                  |)
                |) in
              let~ prefix :=
                M.alloc (|
                  Value.StructRecord
                    "core::ops::index_range::IndexRange"
                    [
                      ("start",
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::ops::index_range::IndexRange",
                            "start"
                          |)
                        |));
                      ("end_", M.read (| mid |))
                    ]
                |) in
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::ops::index_range::IndexRange",
                    "start"
                  |),
                  M.read (| mid |)
                |) in
              prefix
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_take_prefix : M.IsAssociatedFunction Self "take_prefix" take_prefix.
      
      (*
          pub fn take_suffix(&mut self, n: usize) -> Self {
              let mid = if n <= self.len() {
                  // SAFETY: We just checked that this will be between start and end,
                  // and thus the addition cannot overflow.
                  unsafe { self.end.unchecked_sub(n) }
              } else {
                  self.start
              };
              let suffix = Self { start: mid, end: self.end };
              self.end = mid;
              suffix
          }
      *)
      Definition take_suffix (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ mid :=
                M.copy (|
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.le (|
                                  M.read (| n |),
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::exact_size::ExactSizeIterator",
                                      Ty.apply
                                        (Ty.path "&mut")
                                        []
                                        [ Ty.path "core::ops::index_range::IndexRange" ],
                                      [],
                                      "len",
                                      []
                                    |),
                                    [ self ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "usize", "unchecked_sub", [] |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "core::ops::index_range::IndexRange",
                                    "end"
                                  |)
                                |);
                                M.read (| n |)
                              ]
                            |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::ops::index_range::IndexRange",
                            "start"
                          |)))
                    ]
                  |)
                |) in
              let~ suffix :=
                M.alloc (|
                  Value.StructRecord
                    "core::ops::index_range::IndexRange"
                    [
                      ("start", M.read (| mid |));
                      ("end_",
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::ops::index_range::IndexRange",
                            "end"
                          |)
                        |))
                    ]
                |) in
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::ops::index_range::IndexRange",
                    "end"
                  |),
                  M.read (| mid |)
                |) in
              suffix
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_take_suffix : M.IsAssociatedFunction Self "take_suffix" take_suffix.
    End Impl_core_ops_index_range_IndexRange.
    
    Module Impl_core_iter_traits_iterator_Iterator_for_core_ops_index_range_IndexRange.
      Definition Self : Ty.t := Ty.path "core::ops::index_range::IndexRange".
      
      (*     type Item = usize; *)
      Definition _Item : Ty.t := Ty.path "usize".
      
      (*
          fn next(&mut self) -> Option<usize> {
              if self.len() > 0 {
                  // SAFETY: We just checked that the range is non-empty
                  unsafe { Some(self.next_unchecked()) }
              } else {
                  None
              }
          }
      *)
      Definition next (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.gt (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::exact_size::ExactSizeIterator",
                                  Ty.apply
                                    (Ty.path "&mut")
                                    []
                                    [ Ty.path "core::ops::index_range::IndexRange" ],
                                  [],
                                  "len",
                                  []
                                |),
                                [ self ]
                              |),
                              Value.Integer IntegerKind.Usize 0
                            |)
                          |)) 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_associated_function (|
                                Ty.path "core::ops::index_range::IndexRange",
                                "next_unchecked",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn size_hint(&self) -> (usize, Option<usize>) {
              let len = self.len();
              (len, Some(len))
          }
      *)
      Definition size_hint (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::ops::index_range::IndexRange",
                      "len",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.alloc (|
                Value.Tuple
                  [
                    M.read (| len |);
                    Value.StructTuple "core::option::Option::Some" [ M.read (| len |) ]
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn advance_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
              let taken = self.take_prefix(n);
              NonZero::new(n - taken.len()).map_or(Ok(()), Err)
          }
      *)
      Definition advance_by (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ taken :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::ops::index_range::IndexRange",
                      "take_prefix",
                      []
                    |),
                    [ M.read (| self |); M.read (| n |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ],
                    "map_or",
                    [
                      Ty.apply
                        (Ty.path "core::result::Result")
                        []
                        [
                          Ty.tuple [];
                          Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                        ];
                      Ty.function
                        [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ]
                        (Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [
                            Ty.tuple [];
                            Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                          ])
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                        "new",
                        []
                      |),
                      [
                        BinOp.Wrap.sub (|
                          M.read (| n |),
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::ops::index_range::IndexRange",
                              "len",
                              []
                            |),
                            [ taken ]
                          |)
                        |)
                      ]
                    |);
                    Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ];
                    M.constructor_as_closure "core::result::Result::Err"
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty _Item);
            ("next", InstanceField.Method next);
            ("size_hint", InstanceField.Method size_hint);
            ("advance_by", InstanceField.Method advance_by)
          ].
    End Impl_core_iter_traits_iterator_Iterator_for_core_ops_index_range_IndexRange.
    
    Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_ops_index_range_IndexRange.
      Definition Self : Ty.t := Ty.path "core::ops::index_range::IndexRange".
      
      (*
          fn next_back(&mut self) -> Option<usize> {
              if self.len() > 0 {
                  // SAFETY: We just checked that the range is non-empty
                  unsafe { Some(self.next_back_unchecked()) }
              } else {
                  None
              }
          }
      *)
      Definition next_back (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.gt (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::exact_size::ExactSizeIterator",
                                  Ty.apply
                                    (Ty.path "&mut")
                                    []
                                    [ Ty.path "core::ops::index_range::IndexRange" ],
                                  [],
                                  "len",
                                  []
                                |),
                                [ self ]
                              |),
                              Value.Integer IntegerKind.Usize 0
                            |)
                          |)) 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_associated_function (|
                                Ty.path "core::ops::index_range::IndexRange",
                                "next_back_unchecked",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn advance_back_by(&mut self, n: usize) -> Result<(), NonZero<usize>> {
              let taken = self.take_suffix(n);
              NonZero::new(n - taken.len()).map_or(Ok(()), Err)
          }
      *)
      Definition advance_back_by (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ taken :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::ops::index_range::IndexRange",
                      "take_suffix",
                      []
                    |),
                    [ M.read (| self |); M.read (| n |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ],
                    "map_or",
                    [
                      Ty.apply
                        (Ty.path "core::result::Result")
                        []
                        [
                          Ty.tuple [];
                          Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                        ];
                      Ty.function
                        [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ] ]
                        (Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [
                            Ty.tuple [];
                            Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ]
                          ])
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "usize" ],
                        "new",
                        []
                      |),
                      [
                        BinOp.Wrap.sub (|
                          M.read (| n |),
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::ops::index_range::IndexRange",
                              "len",
                              []
                            |),
                            [ taken ]
                          |)
                        |)
                      ]
                    |);
                    Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ];
                    M.constructor_as_closure "core::result::Result::Err"
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::iter::traits::double_ended::DoubleEndedIterator"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("next_back", InstanceField.Method next_back);
            ("advance_back_by", InstanceField.Method advance_back_by)
          ].
    End Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_ops_index_range_IndexRange.
    
    Module Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_ops_index_range_IndexRange.
      Definition Self : Ty.t := Ty.path "core::ops::index_range::IndexRange".
      
      (*
          fn len(&self) -> usize {
              self.len()
          }
      *)
      Definition len (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::ops::index_range::IndexRange",
                "len",
                []
              |),
              [ M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::iter::traits::exact_size::ExactSizeIterator"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("len", InstanceField.Method len) ].
    End Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_ops_index_range_IndexRange.
    
    Module Impl_core_iter_traits_marker_TrustedLen_for_core_ops_index_range_IndexRange.
      Definition Self : Ty.t := Ty.path "core::ops::index_range::IndexRange".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::iter::traits::marker::TrustedLen"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_TrustedLen_for_core_ops_index_range_IndexRange.
    
    Module Impl_core_iter_traits_marker_FusedIterator_for_core_ops_index_range_IndexRange.
      Definition Self : Ty.t := Ty.path "core::ops::index_range::IndexRange".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::iter::traits::marker::FusedIterator"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_FusedIterator_for_core_ops_index_range_IndexRange.
  End index_range.
End ops.
