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

Module array.
  (*
  pub fn repeat<T: Clone, const N: usize>(val: T) -> [T; N] {
      from_trusted_iterator(repeat_n(val, N))
  }
  *)
  Definition repeat (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [ N ], [ T ], [ val ] =>
      ltac:(M.monadic
        (let val := M.alloc (| val |) in
        M.call_closure (|
          M.get_function (|
            "core::array::from_trusted_iterator",
            [ T; Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ T ] ]
          |),
          [
            M.call_closure (|
              M.get_function (| "core::iter::sources::repeat_n::repeat_n", [ T ] |),
              [ M.read (| val |); M.read (| M.get_constant (| "core::array::repeat::N" |) |) ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_repeat : M.IsFunction "core::array::repeat" repeat.
  
  (*
  pub fn from_fn<T, const N: usize, F>(cb: F) -> [T; N]
  where
      F: FnMut(usize) -> T,
  {
      try_from_fn(NeverShortCircuit::wrap_mut_1(cb)).0
  }
  *)
  Definition from_fn (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [ N ], [ T; F ], [ cb ] =>
      ltac:(M.monadic
        (let cb := M.alloc (| cb |) in
        M.read (|
          M.SubPointer.get_struct_tuple_field (|
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::array::try_from_fn",
                  [
                    Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ T ];
                    Ty.associated
                  ]
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ T ],
                      "wrap_mut_1",
                      [ Ty.path "usize"; F ]
                    |),
                    [ M.read (| cb |) ]
                  |)
                ]
              |)
            |),
            "core::ops::try_trait::NeverShortCircuit",
            0
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_from_fn : M.IsFunction "core::array::from_fn" from_fn.
  
  (*
  pub fn try_from_fn<R, const N: usize, F>(cb: F) -> ChangeOutputType<R, [R::Output; N]>
  where
      F: FnMut(usize) -> R,
      R: Try,
      R::Residual: Residual<[R::Output; N]>,
  {
      let mut array = [const { MaybeUninit::uninit() }; N];
      match try_from_fn_erased(&mut array, cb) {
          ControlFlow::Break(r) => FromResidual::from_residual(r),
          ControlFlow::Continue(()) => {
              // SAFETY: All elements of the array were populated.
              try { unsafe { MaybeUninit::array_assume_init(array) } }
          }
      }
  }
  *)
  Definition try_from_fn (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [ N ], [ R; F ], [ cb ] =>
      ltac:(M.monadic
        (let cb := M.alloc (| cb |) in
        M.read (|
          let~ array :=
            M.alloc (|
              repeat (|
                M.read (| M.get_constant (| "core::array::try_from_fn_discriminant" |) |),
                N
              |)
            |) in
          M.match_operator (|
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::array::try_from_fn_erased", [ Ty.associated; R; F ] |),
                [ array; M.read (| cb |) ]
              |)
            |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (|
                      γ,
                      "core::ops::control_flow::ControlFlow::Break",
                      0
                    |) in
                  let r := M.copy (| γ0_0 |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::FromResidual",
                        Ty.associated,
                        [ Ty.associated ],
                        "from_residual",
                        []
                      |),
                      [ M.read (| r |) ]
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (|
                      γ,
                      "core::ops::control_flow::ControlFlow::Continue",
                      0
                    |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::Try",
                        Ty.associated,
                        [],
                        "from_output",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                              []
                              [ Ty.associated ],
                            "array_assume_init",
                            []
                          |),
                          [ M.read (| array |) ]
                        |)
                      ]
                    |)
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_try_from_fn : M.IsFunction "core::array::try_from_fn" try_from_fn.
  
  (*
  pub const fn from_ref<T>(s: &T) -> &[T; 1] {
      // SAFETY: Converting `&T` to `&[T; 1]` is sound.
      unsafe { &*(s as *const T).cast::<[T; 1]>() }
  }
  *)
  Definition from_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ s ] =>
      ltac:(M.monadic
        (let s := M.alloc (| s |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "*const") [] [ T ],
            "cast",
            [ Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 1 ] [ T ] ]
          |),
          [ M.read (| M.use (M.alloc (| M.read (| s |) |)) |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_from_ref : M.IsFunction "core::array::from_ref" from_ref.
  
  (*
  pub const fn from_mut<T>(s: &mut T) -> &mut [T; 1] {
      // SAFETY: Converting `&mut T` to `&mut [T; 1]` is sound.
      unsafe { &mut *(s as *mut T).cast::<[T; 1]>() }
  }
  *)
  Definition from_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T ], [ s ] =>
      ltac:(M.monadic
        (let s := M.alloc (| s |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "*mut") [] [ T ],
            "cast",
            [ Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 1 ] [ T ] ]
          |),
          [ M.read (| M.use (M.alloc (| M.read (| s |) |)) |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_from_mut : M.IsFunction "core::array::from_mut" from_mut.
  
  (* StructTuple
    {
      name := "TryFromSliceError";
      const_params := [];
      ty_params := [];
      fields := [ Ty.tuple [] ];
    } *)
  
  Module Impl_core_fmt_Debug_for_core_array_TryFromSliceError.
    Definition Self : Ty.t := Ty.path "core::array::TryFromSliceError".
    
    (* 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_tuple_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "TryFromSliceError" |);
              M.alloc (|
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "core::array::TryFromSliceError",
                  0
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_array_TryFromSliceError.
  
  Module Impl_core_marker_Copy_for_core_array_TryFromSliceError.
    Definition Self : Ty.t := Ty.path "core::array::TryFromSliceError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_core_array_TryFromSliceError.
  
  Module Impl_core_clone_Clone_for_core_array_TryFromSliceError.
    Definition Self : Ty.t := Ty.path "core::array::TryFromSliceError".
    
    (* 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
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
            |)
          |)))
      | _, _, _ => 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_array_TryFromSliceError.
  
  Module Impl_core_fmt_Display_for_core_array_TryFromSliceError.
    Definition Self : Ty.t := Ty.path "core::array::TryFromSliceError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            #[allow(deprecated)]
            self.description().fmt(f)
        }
    *)
    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_trait_method (| "core::fmt::Display", Ty.path "str", [], "fmt", [] |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::error::Error",
                  Ty.path "core::array::TryFromSliceError",
                  [],
                  "description",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.read (| f |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Display"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Display_for_core_array_TryFromSliceError.
  
  Module Impl_core_error_Error_for_core_array_TryFromSliceError.
    Definition Self : Ty.t := Ty.path "core::array::TryFromSliceError".
    
    (*
        fn description(&self) -> &str {
            "could not convert slice to array"
        }
    *)
    Definition description (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| Value.String "could not convert slice to array" |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("description", InstanceField.Method description) ].
  End Impl_core_error_Error_for_core_array_TryFromSliceError.
  
  Module Impl_core_convert_From_core_convert_Infallible_for_core_array_TryFromSliceError.
    Definition Self : Ty.t := Ty.path "core::array::TryFromSliceError".
    
    (*
        fn from(x: Infallible) -> TryFromSliceError {
            match x {}
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ x ] =>
        ltac:(M.monadic
          (let x := M.alloc (| x |) in
          M.never_to_any (| M.read (| M.match_operator (| x, [] |) |) |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "core::convert::Infallible" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_core_convert_Infallible_for_core_array_TryFromSliceError.
  
  Module Impl_core_convert_AsRef_slice_T_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    (*
        fn as_ref(&self) -> &[T] {
            &self[..]
        }
    *)
    Definition as_ref
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::index::Index",
              Ty.apply (Ty.path "array") [ N ] [ T ],
              [ Ty.path "core::ops::range::RangeFull" ],
              "index",
              []
            |),
            [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::convert::AsRef"
        (Self N T)
        (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
        (* Instance *) [ ("as_ref", InstanceField.Method (as_ref N T)) ].
  End Impl_core_convert_AsRef_slice_T_for_array_N_T.
  
  Module Impl_core_convert_AsMut_slice_T_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    (*
        fn as_mut(&mut self) -> &mut [T] {
            &mut self[..]
        }
    *)
    Definition as_mut
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::index::IndexMut",
              Ty.apply (Ty.path "array") [ N ] [ T ],
              [ Ty.path "core::ops::range::RangeFull" ],
              "index_mut",
              []
            |),
            [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::convert::AsMut"
        (Self N T)
        (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ T ] ]
        (* Instance *) [ ("as_mut", InstanceField.Method (as_mut N T)) ].
  End Impl_core_convert_AsMut_slice_T_for_array_N_T.
  
  Module Impl_core_borrow_Borrow_slice_T_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    (*
        fn borrow(&self) -> &[T] {
            self
        }
    *)
    Definition borrow
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| self |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::borrow::Borrow"
        (Self N T)
        (* Trait polymorphic types *) [ (* Borrowed *) Ty.apply (Ty.path "slice") [] [ T ] ]
        (* Instance *) [ ("borrow", InstanceField.Method (borrow N T)) ].
  End Impl_core_borrow_Borrow_slice_T_for_array_N_T.
  
  Module Impl_core_borrow_BorrowMut_slice_T_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    (*
        fn borrow_mut(&mut self) -> &mut [T] {
            self
        }
    *)
    Definition borrow_mut
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| self |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::borrow::BorrowMut"
        (Self N T)
        (* Trait polymorphic types *) [ (* Borrowed *) Ty.apply (Ty.path "slice") [] [ T ] ]
        (* Instance *) [ ("borrow_mut", InstanceField.Method (borrow_mut N T)) ].
  End Impl_core_borrow_BorrowMut_slice_T_for_array_N_T.
  
  Module Impl_core_convert_TryFrom_where_core_marker_Copy_T_ref__slice_T_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    (*     type Error = TryFromSliceError; *)
    Definition _Error (N : Value.t) (T : Ty.t) : Ty.t := Ty.path "core::array::TryFromSliceError".
    
    (*
        fn try_from(slice: &[T]) -> Result<[T; N], TryFromSliceError> {
            <&Self>::try_from(slice).copied()
        }
    *)
    Definition try_from
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ slice ] =>
        ltac:(M.monadic
          (let slice := M.alloc (| slice |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::result::Result")
                []
                [
                  Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ T ] ];
                  Ty.path "core::array::TryFromSliceError"
                ],
              "copied",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::TryFrom",
                  Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ T ] ],
                  [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ] ],
                  "try_from",
                  []
                |),
                [ M.read (| slice |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::convert::TryFrom"
        (Self N T)
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ] ]
        (* Instance *)
        [
          ("Error", InstanceField.Ty (_Error N T));
          ("try_from", InstanceField.Method (try_from N T))
        ].
  End Impl_core_convert_TryFrom_where_core_marker_Copy_T_ref__slice_T_for_array_N_T.
  
  Module Impl_core_convert_TryFrom_where_core_marker_Copy_T_ref_mut_slice_T_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    (*     type Error = TryFromSliceError; *)
    Definition _Error (N : Value.t) (T : Ty.t) : Ty.t := Ty.path "core::array::TryFromSliceError".
    
    (*
        fn try_from(slice: &mut [T]) -> Result<[T; N], TryFromSliceError> {
            <Self>::try_from(&*slice)
        }
    *)
    Definition try_from
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ slice ] =>
        ltac:(M.monadic
          (let slice := M.alloc (| slice |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::convert::TryFrom",
              Ty.apply (Ty.path "array") [ N ] [ T ],
              [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ] ],
              "try_from",
              []
            |),
            [ M.read (| slice |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::convert::TryFrom"
        (Self N T)
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ T ] ] ]
        (* Instance *)
        [
          ("Error", InstanceField.Ty (_Error N T));
          ("try_from", InstanceField.Method (try_from N T))
        ].
  End Impl_core_convert_TryFrom_where_core_marker_Copy_T_ref_mut_slice_T_for_array_N_T.
  
  Module Impl_core_convert_TryFrom_ref__slice_T_for_ref__array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ T ] ].
    
    (*     type Error = TryFromSliceError; *)
    Definition _Error (N : Value.t) (T : Ty.t) : Ty.t := Ty.path "core::array::TryFromSliceError".
    
    (*
        fn try_from(slice: &'a [T]) -> Result<&'a [T; N], TryFromSliceError> {
            if slice.len() == N {
                let ptr = slice.as_ptr() as *const [T; N];
                // SAFETY: ok because we just checked that the length fits
                unsafe { Ok(&*ptr) }
            } else {
                Err(TryFromSliceError(()))
            }
        }
    *)
    Definition try_from
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ slice ] =>
        ltac:(M.monadic
          (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.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ T ],
                                "len",
                                []
                              |),
                              [ M.read (| slice |) ]
                            |),
                            M.read (| M.get_constant (| "core::array::N" |) |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    let~ ptr :=
                      M.alloc (|
                        M.rust_cast
                          (M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ T ],
                              "as_ptr",
                              []
                            |),
                            [ M.read (| slice |) ]
                          |))
                      |) in
                    M.alloc (|
                      Value.StructTuple "core::result::Result::Ok" [ M.read (| ptr |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [ Value.StructTuple "core::array::TryFromSliceError" [ Value.Tuple [] ] ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::convert::TryFrom"
        (Self N T)
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ] ]
        (* Instance *)
        [
          ("Error", InstanceField.Ty (_Error N T));
          ("try_from", InstanceField.Method (try_from N T))
        ].
  End Impl_core_convert_TryFrom_ref__slice_T_for_ref__array_N_T.
  
  Module Impl_core_convert_TryFrom_ref_mut_slice_T_for_ref_mut_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "array") [ N ] [ T ] ].
    
    (*     type Error = TryFromSliceError; *)
    Definition _Error (N : Value.t) (T : Ty.t) : Ty.t := Ty.path "core::array::TryFromSliceError".
    
    (*
        fn try_from(slice: &'a mut [T]) -> Result<&'a mut [T; N], TryFromSliceError> {
            if slice.len() == N {
                let ptr = slice.as_mut_ptr() as *mut [T; N];
                // SAFETY: ok because we just checked that the length fits
                unsafe { Ok(&mut *ptr) }
            } else {
                Err(TryFromSliceError(()))
            }
        }
    *)
    Definition try_from
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ slice ] =>
        ltac:(M.monadic
          (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.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ T ],
                                "len",
                                []
                              |),
                              [ M.read (| slice |) ]
                            |),
                            M.read (| M.get_constant (| "core::array::N" |) |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    let~ ptr :=
                      M.alloc (|
                        M.rust_cast
                          (M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ T ],
                              "as_mut_ptr",
                              []
                            |),
                            [ M.read (| slice |) ]
                          |))
                      |) in
                    M.alloc (|
                      Value.StructTuple "core::result::Result::Ok" [ M.read (| ptr |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [ Value.StructTuple "core::array::TryFromSliceError" [ Value.Tuple [] ] ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::convert::TryFrom"
        (Self N T)
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ T ] ] ]
        (* Instance *)
        [
          ("Error", InstanceField.Ty (_Error N T));
          ("try_from", InstanceField.Method (try_from N T))
        ].
  End Impl_core_convert_TryFrom_ref_mut_slice_T_for_ref_mut_array_N_T.
  
  Module Impl_core_hash_Hash_where_core_hash_Hash_T_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    (*
        fn hash<H: hash::Hasher>(&self, state: &mut H) {
            Hash::hash(&self[..], state)
        }
    *)
    Definition hash
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [ H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::hash::Hash",
              Ty.apply (Ty.path "slice") [] [ T ],
              [],
              "hash",
              [ H ]
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::index::Index",
                  Ty.apply (Ty.path "array") [ N ] [ T ],
                  [ Ty.path "core::ops::range::RangeFull" ],
                  "index",
                  []
                |),
                [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
              |);
              M.read (| state |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::hash::Hash"
        (Self N T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method (hash N T)) ].
  End Impl_core_hash_Hash_where_core_hash_Hash_T_for_array_N_T.
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            fmt::Debug::fmt(&&self[..], f)
        }
    *)
    Definition fmt
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::fmt::Debug",
              Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
              [],
              "fmt",
              []
            |),
            [
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              |);
              M.read (| f |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self N T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt N T)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_array_N_T.
  
  Module Impl_core_iter_traits_collect_IntoIterator_for_ref__array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ T ] ].
    
    (*     type Item = &'a T; *)
    Definition _Item (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    (*     type IntoIter = Iter<'a, T>; *)
    Definition _IntoIter (N : Value.t) (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ].
    
    (*
        fn into_iter(self) -> Iter<'a, T> {
            self.iter()
        }
    *)
    Definition into_iter
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (| Ty.apply (Ty.path "slice") [] [ T ], "iter", [] |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::collect::IntoIterator"
        (Self N T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item N T));
          ("IntoIter", InstanceField.Ty (_IntoIter N T));
          ("into_iter", InstanceField.Method (into_iter N T))
        ].
  End Impl_core_iter_traits_collect_IntoIterator_for_ref__array_N_T.
  
  Module Impl_core_iter_traits_collect_IntoIterator_for_ref_mut_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "array") [ N ] [ T ] ].
    
    (*     type Item = &'a mut T; *)
    Definition _Item (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
    
    (*     type IntoIter = IterMut<'a, T>; *)
    Definition _IntoIter (N : Value.t) (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ].
    
    (*
        fn into_iter(self) -> IterMut<'a, T> {
            self.iter_mut()
        }
    *)
    Definition into_iter
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (| Ty.apply (Ty.path "slice") [] [ T ], "iter_mut", [] |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::collect::IntoIterator"
        (Self N T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item N T));
          ("IntoIter", InstanceField.Ty (_IntoIter N T));
          ("into_iter", InstanceField.Method (into_iter N T))
        ].
  End Impl_core_iter_traits_collect_IntoIterator_for_ref_mut_array_N_T.
  
  Module Impl_core_ops_index_Index_where_core_ops_index_Index_slice_T_I_I_for_array_N_T.
    Definition Self (N : Value.t) (T I : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    (*     type Output = <[T] as Index<I>>::Output; *)
    Definition _Output (N : Value.t) (T I : Ty.t) : Ty.t := Ty.associated.
    
    (*
        fn index(&self, index: I) -> &Self::Output {
            Index::index(self as &[T], index)
        }
    *)
    Definition index
        (N : Value.t)
        (T I : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T 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::ops::index::Index",
              Ty.apply (Ty.path "slice") [] [ T ],
              [ I ],
              "index",
              []
            |),
            [ M.read (| M.use (M.alloc (| M.read (| self |) |)) |); M.read (| index |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T I : Ty.t),
      M.IsTraitInstance
        "core::ops::index::Index"
        (Self N T I)
        (* Trait polymorphic types *) [ (* Idx *) I ]
        (* Instance *)
        [
          ("Output", InstanceField.Ty (_Output N T I));
          ("index", InstanceField.Method (index N T I))
        ].
  End Impl_core_ops_index_Index_where_core_ops_index_Index_slice_T_I_I_for_array_N_T.
  
  Module Impl_core_ops_index_IndexMut_where_core_ops_index_IndexMut_slice_T_I_I_for_array_N_T.
    Definition Self (N : Value.t) (T I : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    (*
        fn index_mut(&mut self, index: I) -> &mut Self::Output {
            IndexMut::index_mut(self as &mut [T], index)
        }
    *)
    Definition index_mut
        (N : Value.t)
        (T I : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T 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::ops::index::IndexMut",
              Ty.apply (Ty.path "slice") [] [ T ],
              [ I ],
              "index_mut",
              []
            |),
            [ M.read (| M.use (M.alloc (| M.read (| self |) |)) |); M.read (| index |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T I : Ty.t),
      M.IsTraitInstance
        "core::ops::index::IndexMut"
        (Self N T I)
        (* Trait polymorphic types *) [ (* Idx *) I ]
        (* Instance *) [ ("index_mut", InstanceField.Method (index_mut N T I)) ].
  End Impl_core_ops_index_IndexMut_where_core_ops_index_IndexMut_slice_T_I_I_for_array_N_T.
  
  Module Impl_core_cmp_PartialOrd_where_core_cmp_PartialOrd_T_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    (*
        fn partial_cmp(&self, other: &[T; N]) -> Option<Ordering> {
            PartialOrd::partial_cmp(&&self[..], &&other[..])
        }
    *)
    Definition partial_cmp
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
              [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ] ],
              "partial_cmp",
              []
            |),
            [
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| other |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn lt(&self, other: &[T; N]) -> bool {
            PartialOrd::lt(&&self[..], &&other[..])
        }
    *)
    Definition lt
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
              [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ] ],
              "lt",
              []
            |),
            [
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| other |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn le(&self, other: &[T; N]) -> bool {
            PartialOrd::le(&&self[..], &&other[..])
        }
    *)
    Definition le
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
              [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ] ],
              "le",
              []
            |),
            [
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| other |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn ge(&self, other: &[T; N]) -> bool {
            PartialOrd::ge(&&self[..], &&other[..])
        }
    *)
    Definition ge
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
              [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ] ],
              "ge",
              []
            |),
            [
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| other |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn gt(&self, other: &[T; N]) -> bool {
            PartialOrd::gt(&&self[..], &&other[..])
        }
    *)
    Definition gt
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
              [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ] ],
              "gt",
              []
            |),
            [
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| other |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        (Self N T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("partial_cmp", InstanceField.Method (partial_cmp N T));
          ("lt", InstanceField.Method (lt N T));
          ("le", InstanceField.Method (le N T));
          ("ge", InstanceField.Method (ge N T));
          ("gt", InstanceField.Method (gt N T))
        ].
  End Impl_core_cmp_PartialOrd_where_core_cmp_PartialOrd_T_for_array_N_T.
  
  Module Impl_core_cmp_Ord_where_core_cmp_Ord_T_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    (*
        fn cmp(&self, other: &[T; N]) -> Ordering {
            Ord::cmp(&&self[..], &&other[..])
        }
    *)
    Definition cmp
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::Ord",
              Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ],
              [],
              "cmp",
              []
            |),
            [
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              |);
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::Index",
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    [ Ty.path "core::ops::range::RangeFull" ],
                    "index",
                    []
                  |),
                  [ M.read (| other |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::cmp::Ord"
        (Self N T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method (cmp N T)) ].
  End Impl_core_cmp_Ord_where_core_cmp_Ord_T_for_array_N_T.
  
  Module Impl_core_marker_Copy_where_core_marker_Copy_T_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Copy"
        (Self N T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_where_core_marker_Copy_T_for_array_N_T.
  
  Module Impl_core_clone_Clone_where_core_clone_Clone_T_for_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    (*
        fn clone(&self) -> Self {
            SpecArrayClone::clone(self)
        }
    *)
    Definition clone
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (| "core::array::SpecArrayClone", T, [], "clone", [] |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn clone_from(&mut self, other: &Self) {
            self.clone_from_slice(other);
        }
    *)
    Definition clone_from
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ T ],
                    "clone_from_slice",
                    []
                  |),
                  [ M.read (| self |); M.read (| other |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (N : Value.t) (T : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self N T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("clone", InstanceField.Method (clone N T));
          ("clone_from", InstanceField.Method (clone_from N T))
        ].
  End Impl_core_clone_Clone_where_core_clone_Clone_T_for_array_N_T.
  
  (* Trait *)
  (* Empty module 'SpecArrayClone' *)
  
  Module Impl_core_array_SpecArrayClone_where_core_clone_Clone_T_for_T.
    Definition Self (T : Ty.t) : Ty.t := T.
    
    (*
        default fn clone<const N: usize>(array: &[T; N]) -> [T; N] {
            from_trusted_iterator(array.iter().cloned())
        }
    *)
    Definition clone (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [ N ], [], [ array ] =>
        ltac:(M.monadic
          (let array := M.alloc (| array |) in
          M.call_closure (|
            M.get_function (|
              "core::array::from_trusted_iterator",
              [
                T;
                Ty.apply
                  (Ty.path "core::iter::adapters::cloned::Cloned")
                  []
                  [ Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ] ]
              ]
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ],
                  [],
                  "cloned",
                  [ T ]
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.apply (Ty.path "slice") [] [ T ], "iter", [] |),
                    [ M.read (| array |) ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::array::SpecArrayClone"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone T)) ].
  End Impl_core_array_SpecArrayClone_where_core_clone_Clone_T_for_T.
  
  Module Impl_core_array_SpecArrayClone_where_core_marker_Copy_T_for_T.
    Definition Self (T : Ty.t) : Ty.t := T.
    
    (*
        fn clone<const N: usize>(array: &[T; N]) -> [T; N] {
            *array
        }
    *)
    Definition clone (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [ N ], [], [ array ] =>
        ltac:(M.monadic
          (let array := M.alloc (| array |) in
          M.read (| M.read (| array |) |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::array::SpecArrayClone"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone T)) ].
  End Impl_core_array_SpecArrayClone_where_core_marker_Copy_T_for_T.
  
  Module Impl_core_default_Default_where_core_default_Default_T_for_array_Usize_32_T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ T ].
    
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
  End Impl_core_default_Default_where_core_default_Default_T_for_array_Usize_32_T.
  
  Module Impl_core_default_Default_where_core_default_Default_T_for_array_expr_T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply
        (Ty.path "array")
        [ M.unevaluated_const (M.get_constant (| "core::array_discriminant" |)) ]
        [ T ].
    
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |);
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
    (*
                fn default() -> [T; $n] {
                    [$t::default(), $($ts::default()),*]
                }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.Array
            [
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
  End Impl_core_default_Default_where_core_default_Default_T_for_array_expr_T.
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  Module Impl_core_default_Default_for_array_expr_T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply
        (Ty.path "array")
        [ M.unevaluated_const (M.get_constant (| "core::array_discriminant" |)) ]
        [ T ].
    
    (*             fn default() -> [T; $n] { [] } *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] => ltac:(M.monadic (Value.Array []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
  End Impl_core_default_Default_for_array_expr_T.
  
  Module Impl_array_N_T.
    Definition Self (N : Value.t) (T : Ty.t) : Ty.t := Ty.apply (Ty.path "array") [ N ] [ T ].
    
    (*
        pub fn map<F, U>(self, f: F) -> [U; N]
        where
            F: FnMut(T) -> U,
        {
            self.try_map(NeverShortCircuit::wrap_mut_1(f)).0
        }
    *)
    Definition map
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [ F; U ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.SubPointer.get_struct_tuple_field (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "array") [ N ] [ T ],
                    "try_map",
                    [
                      Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ U ];
                      Ty.associated
                    ]
                  |),
                  [
                    M.read (| self |);
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ U ],
                        "wrap_mut_1",
                        [ T; F ]
                      |),
                      [ M.read (| f |) ]
                    |)
                  ]
                |)
              |),
              "core::ops::try_trait::NeverShortCircuit",
              0
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_map :
      forall (N : Value.t) (T : Ty.t),
      M.IsAssociatedFunction (Self N T) "map" (map N T).
    
    (*
        pub fn try_map<R>(self, f: impl FnMut(T) -> R) -> ChangeOutputType<R, [R::Output; N]>
        where
            R: Try<Residual: Residual<[R::Output; N]>>,
        {
            drain_array_with(self, |iter| try_from_trusted_iterator(iter.map(f)))
        }
    *)
    Definition try_map
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [ R; impl_FnMut_T__arrow_R ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_function (|
              "core::array::drain::drain_array_with",
              [
                T;
                Ty.associated;
                Ty.function
                  [ Ty.tuple [ Ty.apply (Ty.path "core::array::drain::Drain") [] [ T ] ] ]
                  Ty.associated
              ]
            |),
            [
              M.read (| self |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let iter := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_function (|
                                    "core::array::try_from_trusted_iterator",
                                    [
                                      Ty.associated;
                                      R;
                                      Ty.apply
                                        (Ty.path "core::iter::adapters::map::Map")
                                        []
                                        [
                                          Ty.apply (Ty.path "core::array::drain::Drain") [] [ T ];
                                          impl_FnMut_T__arrow_R
                                        ]
                                    ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply (Ty.path "core::array::drain::Drain") [] [ T ],
                                        [],
                                        "map",
                                        [ R; impl_FnMut_T__arrow_R ]
                                      |),
                                      [ M.read (| iter |); M.read (| f |) ]
                                    |)
                                  ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_try_map :
      forall (N : Value.t) (T : Ty.t),
      M.IsAssociatedFunction (Self N T) "try_map" (try_map N T).
    
    (*
        pub const fn as_slice(&self) -> &[T] {
            self
        }
    *)
    Definition as_slice
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| self |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_slice :
      forall (N : Value.t) (T : Ty.t),
      M.IsAssociatedFunction (Self N T) "as_slice" (as_slice N T).
    
    (*
        pub fn as_mut_slice(&mut self) -> &mut [T] {
            self
        }
    *)
    Definition as_mut_slice
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| self |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_mut_slice :
      forall (N : Value.t) (T : Ty.t),
      M.IsAssociatedFunction (Self N T) "as_mut_slice" (as_mut_slice N T).
    
    (*
        pub fn each_ref(&self) -> [&T; N] {
            from_trusted_iterator(self.iter())
        }
    *)
    Definition each_ref
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_function (|
              "core::array::from_trusted_iterator",
              [
                Ty.apply (Ty.path "&") [] [ T ];
                Ty.apply (Ty.path "core::slice::iter::Iter") [] [ T ]
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.apply (Ty.path "slice") [] [ T ], "iter", [] |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_each_ref :
      forall (N : Value.t) (T : Ty.t),
      M.IsAssociatedFunction (Self N T) "each_ref" (each_ref N T).
    
    (*
        pub fn each_mut(&mut self) -> [&mut T; N] {
            from_trusted_iterator(self.iter_mut())
        }
    *)
    Definition each_mut
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_function (|
              "core::array::from_trusted_iterator",
              [
                Ty.apply (Ty.path "&mut") [] [ T ];
                Ty.apply (Ty.path "core::slice::iter::IterMut") [] [ T ]
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.apply (Ty.path "slice") [] [ T ], "iter_mut", [] |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_each_mut :
      forall (N : Value.t) (T : Ty.t),
      M.IsAssociatedFunction (Self N T) "each_mut" (each_mut N T).
    
    (*
        pub fn split_array_ref<const M: usize>(&self) -> (&[T; M], &[T]) {
            (&self[..]).split_first_chunk::<M>().unwrap()
        }
    *)
    Definition split_array_ref
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [ M_ ], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [
                  Ty.tuple
                    [
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ M ] [ T ] ];
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ]
                    ]
                ],
              "unwrap",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "slice") [] [ T ],
                  "split_first_chunk",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::index::Index",
                      Ty.apply (Ty.path "array") [ N ] [ T ],
                      [ Ty.path "core::ops::range::RangeFull" ],
                      "index",
                      []
                    |),
                    [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_split_array_ref :
      forall (N : Value.t) (T : Ty.t),
      M.IsAssociatedFunction (Self N T) "split_array_ref" (split_array_ref N T).
    
    (*
        pub fn split_array_mut<const M: usize>(&mut self) -> (&mut [T; M], &mut [T]) {
            (&mut self[..]).split_first_chunk_mut::<M>().unwrap()
        }
    *)
    Definition split_array_mut
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [ M_ ], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [
                  Ty.tuple
                    [
                      Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "array") [ M ] [ T ] ];
                      Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ T ] ]
                    ]
                ],
              "unwrap",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "slice") [] [ T ],
                  "split_first_chunk_mut",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::index::IndexMut",
                      Ty.apply (Ty.path "array") [ N ] [ T ],
                      [ Ty.path "core::ops::range::RangeFull" ],
                      "index_mut",
                      []
                    |),
                    [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_split_array_mut :
      forall (N : Value.t) (T : Ty.t),
      M.IsAssociatedFunction (Self N T) "split_array_mut" (split_array_mut N T).
    
    (*
        pub fn rsplit_array_ref<const M: usize>(&self) -> (&[T], &[T; M]) {
            (&self[..]).split_last_chunk::<M>().unwrap()
        }
    *)
    Definition rsplit_array_ref
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [ M_ ], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [
                  Ty.tuple
                    [
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ T ] ];
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ M ] [ T ] ]
                    ]
                ],
              "unwrap",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "slice") [] [ T ],
                  "split_last_chunk",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::index::Index",
                      Ty.apply (Ty.path "array") [ N ] [ T ],
                      [ Ty.path "core::ops::range::RangeFull" ],
                      "index",
                      []
                    |),
                    [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_rsplit_array_ref :
      forall (N : Value.t) (T : Ty.t),
      M.IsAssociatedFunction (Self N T) "rsplit_array_ref" (rsplit_array_ref N T).
    
    (*
        pub fn rsplit_array_mut<const M: usize>(&mut self) -> (&mut [T], &mut [T; M]) {
            (&mut self[..]).split_last_chunk_mut::<M>().unwrap()
        }
    *)
    Definition rsplit_array_mut
        (N : Value.t)
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self N T in
      match ε, τ, α with
      | [ M_ ], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [
                  Ty.tuple
                    [
                      Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ T ] ];
                      Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "array") [ M ] [ T ] ]
                    ]
                ],
              "unwrap",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "slice") [] [ T ],
                  "split_last_chunk_mut",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::index::IndexMut",
                      Ty.apply (Ty.path "array") [ N ] [ T ],
                      [ Ty.path "core::ops::range::RangeFull" ],
                      "index_mut",
                      []
                    |),
                    [ M.read (| self |); Value.StructTuple "core::ops::range::RangeFull" [] ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_rsplit_array_mut :
      forall (N : Value.t) (T : Ty.t),
      M.IsAssociatedFunction (Self N T) "rsplit_array_mut" (rsplit_array_mut N T).
  End Impl_array_N_T.
  
  (*
  fn from_trusted_iterator<T, const N: usize>(iter: impl UncheckedIterator<Item = T>) -> [T; N] {
      try_from_trusted_iterator(iter.map(NeverShortCircuit)).0
  }
  *)
  Definition from_trusted_iterator (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [ N ], [ T; impl_UncheckedIterator_Item___T_ ], [ iter ] =>
      ltac:(M.monadic
        (let iter := M.alloc (| iter |) in
        M.read (|
          M.SubPointer.get_struct_tuple_field (|
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::array::try_from_trusted_iterator",
                  [
                    T;
                    Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ T ];
                    Ty.apply
                      (Ty.path "core::iter::adapters::map::Map")
                      []
                      [
                        impl_UncheckedIterator_Item___T_;
                        Ty.function
                          [ T ]
                          (Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ T ])
                      ]
                  ]
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      impl_UncheckedIterator_Item___T_,
                      [],
                      "map",
                      [
                        Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ T ];
                        Ty.function
                          [ T ]
                          (Ty.apply (Ty.path "core::ops::try_trait::NeverShortCircuit") [] [ T ])
                      ]
                    |),
                    [
                      M.read (| iter |);
                      M.constructor_as_closure "core::ops::try_trait::NeverShortCircuit"
                    ]
                  |)
                ]
              |)
            |),
            "core::ops::try_trait::NeverShortCircuit",
            0
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_from_trusted_iterator :
    M.IsFunction "core::array::from_trusted_iterator" from_trusted_iterator.
  
  (*
  fn try_from_trusted_iterator<T, R, const N: usize>(
      iter: impl UncheckedIterator<Item = R>,
  ) -> ChangeOutputType<R, [T; N]>
  where
      R: Try<Output = T>,
      R::Residual: Residual<[T; N]>,
  {
      assert!(iter.size_hint().0 >= N);
      fn next<T>(mut iter: impl UncheckedIterator<Item = T>) -> impl FnMut(usize) -> T {
          move |_| {
              // SAFETY: We know that `from_fn` will call this at most N times,
              // and we checked to ensure that we have at least that many items.
              unsafe { iter.next_unchecked() }
          }
      }
  
      try_from_fn(next(iter))
  }
  *)
  Definition try_from_trusted_iterator (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [ N ], [ T; R; impl_UncheckedIterator_Item___R_ ], [ iter ] =>
      ltac:(M.monadic
        (let iter := M.alloc (| iter |) in
        M.read (|
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            BinOp.ge (|
                              M.read (|
                                M.SubPointer.get_tuple_field (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        impl_UncheckedIterator_Item___R_,
                                        [],
                                        "size_hint",
                                        []
                                      |),
                                      [ iter ]
                                    |)
                                  |),
                                  0
                                |)
                              |),
                              M.read (|
                                M.get_constant (| "core::array::try_from_trusted_iterator::N" |)
                              |)
                            |)
                          |)
                        |)) 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: iter.size_hint().0 >= N" |) ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_function (| "core::array::try_from_fn", [ R; Ty.associated ] |),
              [
                M.call_closure (|
                  M.get_function (| "core::array::try_from_trusted_iterator.next", [] |),
                  [ M.read (| iter |) ]
                |)
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_try_from_trusted_iterator :
    M.IsFunction "core::array::try_from_trusted_iterator" try_from_trusted_iterator.
  
  Module try_from_trusted_iterator.
    (*
        fn next<T>(mut iter: impl UncheckedIterator<Item = T>) -> impl FnMut(usize) -> T {
            move |_| {
                // SAFETY: We know that `from_fn` will call this at most N times,
                // and we checked to ensure that we have at least that many items.
                unsafe { iter.next_unchecked() }
            }
        }
    *)
    Definition next (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T; impl_UncheckedIterator_Item___T_ ], [ iter ] =>
        ltac:(M.monadic
          (let iter := M.alloc (| iter |) in
          M.closure
            (fun γ =>
              ltac:(M.monadic
                match γ with
                | [ α0 ] =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| α0 |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::unchecked_iterator::UncheckedIterator",
                                impl_UncheckedIterator_Item___T_,
                                [],
                                "next_unchecked",
                                []
                              |),
                              [ iter ]
                            |)))
                      ]
                    |)))
                | _ => M.impossible "wrong number of arguments"
                end))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_next : M.IsFunction "core::array::try_from_trusted_iterator::next" next.
    
    Module next.
      (* Error OpaqueTy *)
    End next.
  End try_from_trusted_iterator.
  
  (*
  fn try_from_fn_erased<T, R>(
      buffer: &mut [MaybeUninit<T>],
      mut generator: impl FnMut(usize) -> R,
  ) -> ControlFlow<R::Residual>
  where
      R: Try<Output = T>,
  {
      let mut guard = Guard { array_mut: buffer, initialized: 0 };
  
      while guard.initialized < guard.array_mut.len() {
          let item = generator(guard.initialized).branch()?;
  
          // SAFETY: The loop condition ensures we have space to push the item
          unsafe { guard.push_unchecked(item) };
      }
  
      mem::forget(guard);
      ControlFlow::Continue(())
  }
  *)
  Definition try_from_fn_erased (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T; R; impl_FnMut_usize__arrow_R ], [ buffer; generator ] =>
      ltac:(M.monadic
        (let buffer := M.alloc (| buffer |) in
        let generator := M.alloc (| generator |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ guard :=
                M.alloc (|
                  Value.StructRecord
                    "core::array::Guard"
                    [
                      ("array_mut", M.read (| buffer |));
                      ("initialized", Value.Integer IntegerKind.Usize 0)
                    ]
                |) in
              let~ _ :=
                M.loop (|
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.lt (|
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        guard,
                                        "core::array::Guard",
                                        "initialized"
                                      |)
                                    |),
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "slice")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                              []
                                              [ T ]
                                          ],
                                        "len",
                                        []
                                      |),
                                      [
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            guard,
                                            "core::array::Guard",
                                            "array_mut"
                                          |)
                                        |)
                                      ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ item :=
                              M.copy (|
                                M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::Try",
                                        Ty.apply
                                          (Ty.path "core::ops::control_flow::ControlFlow")
                                          []
                                          [ Ty.associated; T ],
                                        [],
                                        "branch",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::Try",
                                            R,
                                            [],
                                            "branch",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::function::FnMut",
                                                impl_FnMut_usize__arrow_R,
                                                [ Ty.tuple [ Ty.path "usize" ] ],
                                                "call_mut",
                                                []
                                              |),
                                              [
                                                generator;
                                                Value.Tuple
                                                  [
                                                    M.read (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        guard,
                                                        "core::array::Guard",
                                                        "initialized"
                                                      |)
                                                    |)
                                                  ]
                                              ]
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |),
                                  [
                                    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::ops::control_flow::ControlFlow")
                                                      []
                                                      [ Ty.associated; Ty.tuple [] ],
                                                    [
                                                      Ty.apply
                                                        (Ty.path
                                                          "core::ops::control_flow::ControlFlow")
                                                        []
                                                        [
                                                          Ty.associated;
                                                          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))
                                  ]
                                |)
                              |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "core::array::Guard") [] [ T ],
                                    "push_unchecked",
                                    []
                                  |),
                                  [ guard; M.read (| item |) ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ _ :=
                                    M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                                  M.alloc (| Value.Tuple [] |)
                                |)
                              |)
                            |)))
                      ]
                    |)))
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::mem::forget",
                      [ Ty.apply (Ty.path "core::array::Guard") [] [ T ] ]
                    |),
                    [ M.read (| guard |) ]
                  |)
                |) in
              M.alloc (|
                Value.StructTuple
                  "core::ops::control_flow::ControlFlow::Continue"
                  [ Value.Tuple [] ]
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_try_from_fn_erased :
    M.IsFunction "core::array::try_from_fn_erased" try_from_fn_erased.
  
  (* StructRecord
    {
      name := "Guard";
      const_params := [];
      ty_params := [ "T" ];
      fields :=
        [
          ("array_mut",
            Ty.apply
              (Ty.path "&mut")
              []
              [
                Ty.apply
                  (Ty.path "slice")
                  []
                  [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ]
              ]);
          ("initialized", Ty.path "usize")
        ];
    } *)
  
  Module Impl_core_array_Guard_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::array::Guard") [] [ T ].
    
    (*
        pub unsafe fn push_unchecked(&mut self, item: T) {
            // SAFETY: If `initialized` was correct before and the caller does not
            // invoke this method more than N times then writes will be in-bounds
            // and slots will not be initialized more than once.
            unsafe {
                self.array_mut.get_unchecked_mut(self.initialized).write(item);
                self.initialized = self.initialized.unchecked_add(1);
            }
        }
    *)
    Definition push_unchecked
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; item ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let item := M.alloc (| item |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                    "write",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "slice")
                          []
                          [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ],
                        "get_unchecked_mut",
                        [ Ty.path "usize" ]
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::array::Guard",
                            "array_mut"
                          |)
                        |);
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::array::Guard",
                            "initialized"
                          |)
                        |)
                      ]
                    |);
                    M.read (| item |)
                  ]
                |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::array::Guard",
                  "initialized"
                |),
                M.call_closure (|
                  M.get_associated_function (| Ty.path "usize", "unchecked_add", [] |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::array::Guard",
                        "initialized"
                      |)
                    |);
                    Value.Integer IntegerKind.Usize 1
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_push_unchecked :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "push_unchecked" (push_unchecked T).
  End Impl_core_array_Guard_T.
  
  Module Impl_core_ops_drop_Drop_for_core_array_Guard_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::array::Guard") [] [ T ].
    
    (*
        fn drop(&mut self) {
            debug_assert!(self.initialized <= self.array_mut.len());
    
            // SAFETY: this slice will contain only initialized objects.
            unsafe {
                crate::ptr::drop_in_place(MaybeUninit::slice_assume_init_mut(
                    self.array_mut.get_unchecked_mut(..self.initialized),
                ));
            }
        }
    *)
    Definition drop (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      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.le (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "core::array::Guard",
                                              "initialized"
                                            |)
                                          |),
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "slice")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                                    []
                                                    [ T ]
                                                ],
                                              "len",
                                              []
                                            |),
                                            [
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "core::array::Guard",
                                                  "array_mut"
                                                |)
                                              |)
                                            ]
                                          |)
                                        |)
                                      |)
                                    |)) 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.initialized <= self.array_mut.len()"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::ptr::drop_in_place",
                    [ Ty.apply (Ty.path "slice") [] [ T ] ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                        "slice_assume_init_mut",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "slice")
                              []
                              [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
                              ],
                            "get_unchecked_mut",
                            [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ]
                            ]
                          |),
                          [
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::array::Guard",
                                "array_mut"
                              |)
                            |);
                            Value.StructRecord
                              "core::ops::range::RangeTo"
                              [
                                ("end_",
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "core::array::Guard",
                                      "initialized"
                                    |)
                                  |))
                              ]
                          ]
                        |)
                      ]
                    |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::drop::Drop"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("drop", InstanceField.Method (drop T)) ].
  End Impl_core_ops_drop_Drop_for_core_array_Guard_T.
  
  (*
  pub(crate) fn iter_next_chunk<T, const N: usize>(
      iter: &mut impl Iterator<Item = T>,
  ) -> Result<[T; N], IntoIter<T, N>> {
      let mut array = [const { MaybeUninit::uninit() }; N];
      let r = iter_next_chunk_erased(&mut array, iter);
      match r {
          Ok(()) => {
              // SAFETY: All elements of `array` were populated.
              Ok(unsafe { MaybeUninit::array_assume_init(array) })
          }
          Err(initialized) => {
              // SAFETY: Only the first `initialized` elements were populated
              Err(unsafe { IntoIter::new_unchecked(array, 0..initialized) })
          }
      }
  }
  *)
  Definition iter_next_chunk (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [ N ], [ T; impl_Iterator_Item___T_ ], [ iter ] =>
      ltac:(M.monadic
        (let iter := M.alloc (| iter |) in
        M.read (|
          let~ array :=
            M.alloc (|
              repeat (|
                M.read (| M.get_constant (| "core::array::iter_next_chunk_discriminant" |) |),
                N
              |)
            |) in
          let~ r :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::array::iter_next_chunk_erased",
                  [ T; impl_Iterator_Item___T_ ]
                |),
                [ array; M.read (| iter |) ]
              |)
            |) in
          M.match_operator (|
            r,
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Ok"
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ],
                            "array_assume_init",
                            []
                          |),
                          [ M.read (| array |) ]
                        |)
                      ]
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                  let initialized := M.copy (| γ0_0 |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Err"
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::array::iter::IntoIter") [ N ] [ T ],
                            "new_unchecked",
                            []
                          |),
                          [
                            M.read (| array |);
                            Value.StructRecord
                              "core::ops::range::Range"
                              [
                                ("start", Value.Integer IntegerKind.Usize 0);
                                ("end_", M.read (| initialized |))
                              ]
                          ]
                        |)
                      ]
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_iter_next_chunk : M.IsFunction "core::array::iter_next_chunk" iter_next_chunk.
  
  (*
  fn iter_next_chunk_erased<T>(
      buffer: &mut [MaybeUninit<T>],
      iter: &mut impl Iterator<Item = T>,
  ) -> Result<(), usize> {
      let mut guard = Guard { array_mut: buffer, initialized: 0 };
      while guard.initialized < guard.array_mut.len() {
          let Some(item) = iter.next() else {
              // Unlike `try_from_fn_erased`, we want to keep the partial results,
              // so we need to defuse the guard instead of using `?`.
              let initialized = guard.initialized;
              mem::forget(guard);
              return Err(initialized);
          };
  
          // SAFETY: The loop condition ensures we have space to push the item
          unsafe { guard.push_unchecked(item) };
      }
  
      mem::forget(guard);
      Ok(())
  }
  *)
  Definition iter_next_chunk_erased (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ T; impl_Iterator_Item___T_ ], [ buffer; iter ] =>
      ltac:(M.monadic
        (let buffer := M.alloc (| buffer |) in
        let iter := M.alloc (| iter |) in
        M.read (|
          let~ guard :=
            M.alloc (|
              Value.StructRecord
                "core::array::Guard"
                [
                  ("array_mut", M.read (| buffer |));
                  ("initialized", Value.Integer IntegerKind.Usize 0)
                ]
            |) in
          let~ _ :=
            M.loop (|
              ltac:(M.monadic
                (M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (|
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    guard,
                                    "core::array::Guard",
                                    "initialized"
                                  |)
                                |),
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "core::mem::maybe_uninit::MaybeUninit")
                                          []
                                          [ T ]
                                      ],
                                    "len",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        guard,
                                        "core::array::Guard",
                                        "array_mut"
                                      |)
                                    |)
                                  ]
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                impl_Iterator_Item___T_,
                                [],
                                "next",
                                []
                              |),
                              [ M.read (| iter |) ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let item := M.copy (| γ0_0 |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "core::array::Guard") [] [ T ],
                                        "push_unchecked",
                                        []
                                      |),
                                      [ guard; M.read (| item |) ]
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                          ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ _ :=
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                              M.alloc (| Value.Tuple [] |)
                            |)
                          |)
                        |)))
                  ]
                |)))
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::mem::forget",
                  [ Ty.apply (Ty.path "core::array::Guard") [] [ T ] ]
                |),
                [ M.read (| guard |) ]
              |)
            |) in
          M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_iter_next_chunk_erased :
    M.IsFunction "core::array::iter_next_chunk_erased" iter_next_chunk_erased.
End array.
