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

Module char.
  Module decode.
    (* StructRecord
      {
        name := "DecodeUtf16";
        const_params := [];
        ty_params := [ "I" ];
        fields :=
          [ ("iter", I); ("buf", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u16" ]) ];
      } *)
    
    Module Impl_core_clone_Clone_where_core_clone_Clone_I_where_core_iter_traits_iterator_Iterator_I_for_core_char_decode_DecodeUtf16_I.
      Definition Self (I : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::char::decode::DecodeUtf16") [] [ I ].
      
      (* Clone *)
      Definition clone (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self I in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "core::char::decode::DecodeUtf16"
              [
                ("iter",
                  M.call_closure (|
                    M.get_trait_method (| "core::clone::Clone", I, [], "clone", [] |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::char::decode::DecodeUtf16",
                        "iter"
                      |)
                    ]
                  |));
                ("buf",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u16" ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::char::decode::DecodeUtf16",
                        "buf"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (I : Ty.t),
        M.IsTraitInstance
          "core::clone::Clone"
          (Self I)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method (clone I)) ].
    End Impl_core_clone_Clone_where_core_clone_Clone_I_where_core_iter_traits_iterator_Iterator_I_for_core_char_decode_DecodeUtf16_I.
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_I_where_core_iter_traits_iterator_Iterator_I_for_core_char_decode_DecodeUtf16_I.
      Definition Self (I : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::char::decode::DecodeUtf16") [] [ I ].
      
      (* Debug *)
      Definition fmt (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self I 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_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_struct_field2_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "DecodeUtf16" |);
                M.read (| Value.String "iter" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::char::decode::DecodeUtf16",
                  "iter"
                |);
                M.read (| Value.String "buf" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::char::decode::DecodeUtf16",
                    "buf"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (I : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self I)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt I)) ].
    End Impl_core_fmt_Debug_where_core_fmt_Debug_I_where_core_iter_traits_iterator_Iterator_I_for_core_char_decode_DecodeUtf16_I.
    
    (* StructRecord
      {
        name := "DecodeUtf16Error";
        const_params := [];
        ty_params := [];
        fields := [ ("code", Ty.path "u16") ];
      } *)
    
    Module Impl_core_fmt_Debug_for_core_char_decode_DecodeUtf16Error.
      Definition Self : Ty.t := Ty.path "core::char::decode::DecodeUtf16Error".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_struct_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "DecodeUtf16Error" |);
                M.read (| Value.String "code" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::char::decode::DecodeUtf16Error",
                    "code"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_char_decode_DecodeUtf16Error.
    
    Module Impl_core_clone_Clone_for_core_char_decode_DecodeUtf16Error.
      Definition Self : Ty.t := Ty.path "core::char::decode::DecodeUtf16Error".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "core::char::decode::DecodeUtf16Error"
              [
                ("code",
                  M.call_closure (|
                    M.get_trait_method (| "core::clone::Clone", Ty.path "u16", [], "clone", [] |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::char::decode::DecodeUtf16Error",
                        "code"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => 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_char_decode_DecodeUtf16Error.
    
    Module Impl_core_cmp_Eq_for_core_char_decode_DecodeUtf16Error.
      Definition Self : Ty.t := Ty.path "core::char::decode::DecodeUtf16Error".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_char_decode_DecodeUtf16Error.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_char_decode_DecodeUtf16Error.
      Definition Self : Ty.t := Ty.path "core::char::decode::DecodeUtf16Error".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_char_decode_DecodeUtf16Error.
    
    Module Impl_core_cmp_PartialEq_for_core_char_decode_DecodeUtf16Error.
      Definition Self : Ty.t := Ty.path "core::char::decode::DecodeUtf16Error".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            BinOp.eq (|
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::char::decode::DecodeUtf16Error",
                  "code"
                |)
              |),
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "core::char::decode::DecodeUtf16Error",
                  "code"
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_char_decode_DecodeUtf16Error.
    
    (*
    pub(super) fn decode_utf16<I: IntoIterator<Item = u16>>(iter: I) -> DecodeUtf16<I::IntoIter> {
        DecodeUtf16 { iter: iter.into_iter(), buf: None }
    }
    *)
    Definition decode_utf16 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ _ as I ], [ iter ] =>
        ltac:(M.monadic
          (let iter := M.alloc (| iter |) in
          Value.StructRecord
            "core::char::decode::DecodeUtf16"
            [
              ("iter",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::collect::IntoIterator",
                    I,
                    [],
                    "into_iter",
                    []
                  |),
                  [ M.read (| iter |) ]
                |));
              ("buf", Value.StructTuple "core::option::Option::None" [])
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_decode_utf16 : M.IsFunction "core::char::decode::decode_utf16" decode_utf16.
    
    Module Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_for_core_char_decode_DecodeUtf16_I.
      Definition Self (I : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::char::decode::DecodeUtf16") [] [ I ].
      
      (*     type Item = Result<char, DecodeUtf16Error>; *)
      Definition _Item (I : Ty.t) : Ty.t :=
        Ty.apply
          (Ty.path "core::result::Result")
          []
          [ Ty.path "char"; Ty.path "core::char::decode::DecodeUtf16Error" ].
      
      (*
          fn next(&mut self) -> Option<Result<char, DecodeUtf16Error>> {
              let u = match self.buf.take() {
                  Some(buf) => buf,
                  None => self.iter.next()?,
              };
      
              if !u.is_utf16_surrogate() {
                  // SAFETY: not a surrogate
                  Some(Ok(unsafe { char::from_u32_unchecked(u as u32) }))
              } else if u >= 0xDC00 {
                  // a trailing surrogate
                  Some(Err(DecodeUtf16Error { code: u }))
              } else {
                  let u2 = match self.iter.next() {
                      Some(u2) => u2,
                      // eof
                      None => return Some(Err(DecodeUtf16Error { code: u })),
                  };
                  if u2 < 0xDC00 || u2 > 0xDFFF {
                      // not a trailing surrogate so we're not a valid
                      // surrogate pair, so rewind to redecode u2 next time.
                      self.buf = Some(u2);
                      return Some(Err(DecodeUtf16Error { code: u }));
                  }
      
                  // all ok, so lets decode it.
                  let c = (((u & 0x3ff) as u32) << 10 | (u2 & 0x3ff) as u32) + 0x1_0000;
                  // SAFETY: we checked that it's a legal unicode value
                  Some(Ok(unsafe { char::from_u32_unchecked(c) }))
              }
          }
      *)
      Definition next (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self I in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ u :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u16" ],
                              "take",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::char::decode::DecodeUtf16",
                                "buf"
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let buf := M.copy (| γ0_0 |) in
                              buf));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::try_trait::Try",
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "u16" ],
                                      [],
                                      "branch",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          I,
                                          [],
                                          "next",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "core::char::decode::DecodeUtf16",
                                            "iter"
                                          |)
                                        ]
                                      |)
                                    ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::ops::control_flow::ControlFlow::Break",
                                          0
                                        |) in
                                      let residual := M.copy (| γ0_0 |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            M.return_ (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::try_trait::FromResidual",
                                                  Ty.apply
                                                    (Ty.path "core::option::Option")
                                                    []
                                                    [
                                                      Ty.apply
                                                        (Ty.path "core::result::Result")
                                                        []
                                                        [
                                                          Ty.path "char";
                                                          Ty.path
                                                            "core::char::decode::DecodeUtf16Error"
                                                        ]
                                                    ],
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::option::Option")
                                                      []
                                                      [ Ty.path "core::convert::Infallible" ]
                                                  ],
                                                  "from_residual",
                                                  []
                                                |),
                                                [ M.read (| residual |) ]
                                              |)
                                            |)
                                          |)
                                        |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::ops::control_flow::ControlFlow::Continue",
                                          0
                                        |) in
                                      let val := M.copy (| γ0_0 |) in
                                      val))
                                ]
                              |)))
                        ]
                      |)
                    |) in
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "u16",
                                      "is_utf16_surrogate",
                                      []
                                    |),
                                    [ M.read (| u |) ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            Value.StructTuple
                              "core::option::Option::Some"
                              [
                                Value.StructTuple
                                  "core::result::Result::Ok"
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "char",
                                        "from_u32_unchecked",
                                        []
                                      |),
                                      [ M.rust_cast (M.read (| u |)) ]
                                    |)
                                  ]
                              ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.ge (|
                                          M.read (| u |),
                                          Value.Integer IntegerKind.U16 56320
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    Value.StructTuple
                                      "core::option::Option::Some"
                                      [
                                        Value.StructTuple
                                          "core::result::Result::Err"
                                          [
                                            Value.StructRecord
                                              "core::char::decode::DecodeUtf16Error"
                                              [ ("code", M.read (| u |)) ]
                                          ]
                                      ]
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let~ u2 :=
                                    M.copy (|
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::iterator::Iterator",
                                              I,
                                              [],
                                              "next",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "core::char::decode::DecodeUtf16",
                                                "iter"
                                              |)
                                            ]
                                          |)
                                        |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::option::Option::Some",
                                                  0
                                                |) in
                                              let u2 := M.copy (| γ0_0 |) in
                                              u2));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let _ :=
                                                M.is_struct_tuple (|
                                                  γ,
                                                  "core::option::Option::None"
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (|
                                                  M.read (|
                                                    M.return_ (|
                                                      Value.StructTuple
                                                        "core::option::Option::Some"
                                                        [
                                                          Value.StructTuple
                                                            "core::result::Result::Err"
                                                            [
                                                              Value.StructRecord
                                                                "core::char::decode::DecodeUtf16Error"
                                                                [ ("code", M.read (| u |)) ]
                                                            ]
                                                        ]
                                                    |)
                                                  |)
                                                |)
                                              |)))
                                        ]
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  LogicalOp.or (|
                                                    BinOp.lt (|
                                                      M.read (| u2 |),
                                                      Value.Integer IntegerKind.U16 56320
                                                    |),
                                                    ltac:(M.monadic
                                                      (BinOp.gt (|
                                                        M.read (| u2 |),
                                                        Value.Integer IntegerKind.U16 57343
                                                      |)))
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  let~ _ :=
                                                    M.write (|
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "core::char::decode::DecodeUtf16",
                                                        "buf"
                                                      |),
                                                      Value.StructTuple
                                                        "core::option::Option::Some"
                                                        [ M.read (| u2 |) ]
                                                    |) in
                                                  M.return_ (|
                                                    Value.StructTuple
                                                      "core::option::Option::Some"
                                                      [
                                                        Value.StructTuple
                                                          "core::result::Result::Err"
                                                          [
                                                            Value.StructRecord
                                                              "core::char::decode::DecodeUtf16Error"
                                                              [ ("code", M.read (| u |)) ]
                                                          ]
                                                      ]
                                                  |)
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  let~ c :=
                                    M.alloc (|
                                      BinOp.Wrap.add (|
                                        BinOp.bit_or
                                          (BinOp.Wrap.shl (|
                                            M.rust_cast
                                              (BinOp.bit_and
                                                (M.read (| u |))
                                                (Value.Integer IntegerKind.U16 1023)),
                                            Value.Integer IntegerKind.I32 10
                                          |))
                                          (M.rust_cast
                                            (BinOp.bit_and
                                              (M.read (| u2 |))
                                              (Value.Integer IntegerKind.U16 1023))),
                                        Value.Integer IntegerKind.U32 65536
                                      |)
                                    |) in
                                  M.alloc (|
                                    Value.StructTuple
                                      "core::option::Option::Some"
                                      [
                                        Value.StructTuple
                                          "core::result::Result::Ok"
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "char",
                                                "from_u32_unchecked",
                                                []
                                              |),
                                              [ M.read (| c |) ]
                                            |)
                                          ]
                                      ]
                                  |)))
                            ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn size_hint(&self) -> (usize, Option<usize>) {
              let (low, high) = self.iter.size_hint();
      
              let (low_buf, high_buf) = match self.buf {
                  // buf is empty, no additional elements from it.
                  None => (0, 0),
                  // `u` is a non surrogate, so it's always an additional character.
                  Some(u) if !u.is_utf16_surrogate() => (1, 1),
                  // `u` is a leading surrogate (it can never be a trailing surrogate and
                  // it's a surrogate due to the previous branch) and `self.iter` is empty.
                  //
                  // `u` can't be paired, since the `self.iter` is empty,
                  // so it will always become an additional element (error).
                  Some(_u) if high == Some(0) => (1, 1),
                  // `u` is a leading surrogate and `iter` may be non-empty.
                  //
                  // `u` can either pair with a trailing surrogate, in which case no additional elements
                  // are produced, or it can become an error, in which case it's an additional character (error).
                  Some(_u) => (0, 1),
              };
      
              // `self.iter` could contain entirely valid surrogates (2 elements per
              // char), or entirely non-surrogates (1 element per char).
              //
              // On odd lower bound, at least one element must stay unpaired
              // (with other elements from `self.iter`), so we round up.
              let low = low.div_ceil(2) + low_buf;
              let high = high.and_then(|h| h.checked_add(high_buf));
      
              (low, high)
          }
      *)
      Definition size_hint (I : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self I in
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      I,
                      [],
                      "size_hint",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::char::decode::DecodeUtf16",
                        "iter"
                      |)
                    ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let low := M.copy (| γ0_0 |) in
                      let high := M.copy (| γ0_1 |) in
                      M.match_operator (|
                        M.match_operator (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "core::char::decode::DecodeUtf16",
                            "buf"
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                M.alloc (|
                                  Value.Tuple
                                    [
                                      Value.Integer IntegerKind.Usize 0;
                                      Value.Integer IntegerKind.Usize 0
                                    ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let u := M.copy (| γ0_0 |) in
                                let γ :=
                                  M.alloc (|
                                    UnOp.not (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "u16",
                                          "is_utf16_surrogate",
                                          []
                                        |),
                                        [ M.read (| u |) ]
                                      |)
                                    |)
                                  |) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  Value.Tuple
                                    [
                                      Value.Integer IntegerKind.Usize 1;
                                      Value.Integer IntegerKind.Usize 1
                                    ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let _u := M.copy (| γ0_0 |) in
                                let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [ Ty.path "usize" ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.path "usize" ]
                                        ],
                                        "eq",
                                        []
                                      |),
                                      [
                                        high;
                                        M.alloc (|
                                          Value.StructTuple
                                            "core::option::Option::Some"
                                            [ Value.Integer IntegerKind.Usize 0 ]
                                        |)
                                      ]
                                    |)
                                  |) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  Value.Tuple
                                    [
                                      Value.Integer IntegerKind.Usize 1;
                                      Value.Integer IntegerKind.Usize 1
                                    ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::option::Option::Some",
                                    0
                                  |) in
                                let _u := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  Value.Tuple
                                    [
                                      Value.Integer IntegerKind.Usize 0;
                                      Value.Integer IntegerKind.Usize 1
                                    ]
                                |)))
                          ]
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                              let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                              let low_buf := M.copy (| γ0_0 |) in
                              let high_buf := M.copy (| γ0_1 |) in
                              let~ low :=
                                M.alloc (|
                                  BinOp.Wrap.add (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "usize",
                                        "div_ceil",
                                        []
                                      |),
                                      [ M.read (| low |); Value.Integer IntegerKind.Usize 2 ]
                                    |),
                                    M.read (| low_buf |)
                                  |)
                                |) in
                              let~ high :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "usize" ],
                                      "and_then",
                                      [
                                        Ty.path "usize";
                                        Ty.function
                                          [ Ty.tuple [ Ty.path "usize" ] ]
                                          (Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.path "usize" ])
                                      ]
                                    |),
                                    [
                                      M.read (| high |);
                                      M.closure
                                        (fun γ =>
                                          ltac:(M.monadic
                                            match γ with
                                            | [ α0 ] =>
                                              ltac:(M.monadic
                                                (M.match_operator (|
                                                  M.alloc (| α0 |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let h := M.copy (| γ |) in
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "usize",
                                                            "checked_add",
                                                            []
                                                          |),
                                                          [ M.read (| h |); M.read (| high_buf |) ]
                                                        |)))
                                                  ]
                                                |)))
                                            | _ => M.impossible "wrong number of arguments"
                                            end))
                                    ]
                                  |)
                                |) in
                              M.alloc (| Value.Tuple [ M.read (| low |); M.read (| high |) ] |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (I : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::iterator::Iterator"
          (Self I)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Item", InstanceField.Ty (_Item I));
            ("next", InstanceField.Method (next I));
            ("size_hint", InstanceField.Method (size_hint I))
          ].
    End Impl_core_iter_traits_iterator_Iterator_where_core_iter_traits_iterator_Iterator_I_for_core_char_decode_DecodeUtf16_I.
    
    Module Impl_core_iter_traits_marker_FusedIterator_where_core_iter_traits_iterator_Iterator_I_where_core_iter_traits_marker_FusedIterator_I_for_core_char_decode_DecodeUtf16_I.
      Definition Self (I : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "core::char::decode::DecodeUtf16") [] [ I ].
      
      Axiom Implements :
        forall (I : Ty.t),
        M.IsTraitInstance
          "core::iter::traits::marker::FusedIterator"
          (Self I)
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_iter_traits_marker_FusedIterator_where_core_iter_traits_iterator_Iterator_I_where_core_iter_traits_marker_FusedIterator_I_for_core_char_decode_DecodeUtf16_I.
    
    Module Impl_core_char_decode_DecodeUtf16Error.
      Definition Self : Ty.t := Ty.path "core::char::decode::DecodeUtf16Error".
      
      (*
          pub fn unpaired_surrogate(&self) -> u16 {
              self.code
          }
      *)
      Definition unpaired_surrogate (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::char::decode::DecodeUtf16Error",
                "code"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_unpaired_surrogate :
        M.IsAssociatedFunction Self "unpaired_surrogate" unpaired_surrogate.
    End Impl_core_char_decode_DecodeUtf16Error.
    
    Module Impl_core_fmt_Display_for_core_char_decode_DecodeUtf16Error.
      Definition Self : Ty.t := Ty.path "core::char::decode::DecodeUtf16Error".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              write!(f, "unpaired surrogate found: {:x}", self.code)
          }
      *)
      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", "write_fmt", [] |),
              [
                M.read (| f |);
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                  [
                    M.alloc (|
                      Value.Array [ M.read (| Value.String "unpaired surrogate found: " |) ]
                    |);
                    M.alloc (|
                      Value.Array
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::rt::Argument",
                              "new_lower_hex",
                              [ Ty.path "u16" ]
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "core::char::decode::DecodeUtf16Error",
                                "code"
                              |)
                            ]
                          |)
                        ]
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => 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_char_decode_DecodeUtf16Error.
    
    Module Impl_core_error_Error_for_core_char_decode_DecodeUtf16Error.
      Definition Self : Ty.t := Ty.path "core::char::decode::DecodeUtf16Error".
      
      (*
          fn description(&self) -> &str {
              "unpaired surrogate found"
          }
      *)
      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 "unpaired surrogate found" |)))
        | _, _, _ => 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_char_decode_DecodeUtf16Error.
  End decode.
End char.
