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

Module char.
  Module convert.
    (*
    pub(super) const fn from_u32(i: u32) -> Option<char> {
        // FIXME(const-hack): once Result::ok is const fn, use it here
        match char_try_from_u32(i) {
            Ok(c) => Some(c),
            Err(_) => None,
        }
    }
    *)
    Definition from_u32 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ i ] =>
        ltac:(M.monadic
          (let i := M.alloc (| i |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::char::convert::char_try_from_u32", [] |),
                  [ M.read (| i |) ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let c := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple "core::option::Option::Some" [ M.read (| c |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_u32 : M.IsFunction "core::char::convert::from_u32" from_u32.
    
    (*
    pub(super) const unsafe fn from_u32_unchecked(i: u32) -> char {
        // SAFETY: the caller must guarantee that `i` is a valid char value.
        unsafe {
            assert_unsafe_precondition!(
                check_language_ub,
                "invalid value for `char`",
                (i: u32 = i) => char_try_from_u32(i).is_ok()
            );
            transmute(i)
        }
    }
    *)
    Definition from_u32_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ i ] =>
        ltac:(M.monadic
          (let i := M.alloc (| i |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_function (| "core::ub_checks::check_language_ub", [] |),
                              []
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (|
                              "core::char::convert::from_u32_unchecked.precondition_check",
                              []
                            |),
                            [ M.read (| i |) ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::transmute",
                  [ Ty.path "u32"; Ty.path "char" ]
                |),
                [ M.read (| i |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_u32_unchecked :
      M.IsFunction "core::char::convert::from_u32_unchecked" from_u32_unchecked.
    
    Module Impl_core_convert_From_char_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*
          fn from(c: char) -> Self {
              c as u32
          }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ c ] =>
          ltac:(M.monadic
            (let c := M.alloc (| c |) in
            M.rust_cast (M.read (| c |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "char" ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_char_for_u32.
    
    Module Impl_core_convert_From_char_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*
          fn from(c: char) -> Self {
              // The char is casted to the value of the code point, then zero-extended to 64 bit.
              // See [https://doc.rust-lang.org/reference/expressions/operator-expr.html#semantics]
              c as u64
          }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ c ] =>
          ltac:(M.monadic
            (let c := M.alloc (| c |) in
            M.rust_cast (M.read (| c |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "char" ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_char_for_u64.
    
    Module Impl_core_convert_From_char_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*
          fn from(c: char) -> Self {
              // The char is casted to the value of the code point, then zero-extended to 128 bit.
              // See [https://doc.rust-lang.org/reference/expressions/operator-expr.html#semantics]
              c as u128
          }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ c ] =>
          ltac:(M.monadic
            (let c := M.alloc (| c |) in
            M.rust_cast (M.read (| c |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "char" ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_char_for_u128.
    
    Module Impl_core_convert_TryFrom_char_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*     type Error = TryFromCharError; *)
      Definition _Error : Ty.t := Ty.path "core::char::TryFromCharError".
      
      (*
          fn try_from(c: char) -> Result<u8, Self::Error> {
              u8::try_from(u32::from(c)).map_err(|_| TryFromCharError(()))
          }
      *)
      Definition try_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ c ] =>
          ltac:(M.monadic
            (let c := M.alloc (| c |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [ Ty.path "u8"; Ty.path "core::num::error::TryFromIntError" ],
                "map_err",
                [
                  Ty.path "core::char::TryFromCharError";
                  Ty.function
                    [ Ty.tuple [ Ty.path "core::num::error::TryFromIntError" ] ]
                    (Ty.path "core::char::TryFromCharError")
                ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::TryFrom",
                    Ty.path "u8",
                    [ Ty.path "u32" ],
                    "try_from",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::convert::From",
                        Ty.path "u32",
                        [ Ty.path "char" ],
                        "from",
                        []
                      |),
                      [ M.read (| c |) ]
                    |)
                  ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (Value.StructTuple
                                    "core::char::TryFromCharError"
                                    [ Value.Tuple [] ]))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::TryFrom"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "char" ]
          (* Instance *)
          [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
    End Impl_core_convert_TryFrom_char_for_u8.
    
    Module Impl_core_convert_TryFrom_char_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*     type Error = TryFromCharError; *)
      Definition _Error : Ty.t := Ty.path "core::char::TryFromCharError".
      
      (*
          fn try_from(c: char) -> Result<u16, Self::Error> {
              u16::try_from(u32::from(c)).map_err(|_| TryFromCharError(()))
          }
      *)
      Definition try_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ c ] =>
          ltac:(M.monadic
            (let c := M.alloc (| c |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [ Ty.path "u16"; Ty.path "core::num::error::TryFromIntError" ],
                "map_err",
                [
                  Ty.path "core::char::TryFromCharError";
                  Ty.function
                    [ Ty.tuple [ Ty.path "core::num::error::TryFromIntError" ] ]
                    (Ty.path "core::char::TryFromCharError")
                ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::TryFrom",
                    Ty.path "u16",
                    [ Ty.path "u32" ],
                    "try_from",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::convert::From",
                        Ty.path "u32",
                        [ Ty.path "char" ],
                        "from",
                        []
                      |),
                      [ M.read (| c |) ]
                    |)
                  ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (Value.StructTuple
                                    "core::char::TryFromCharError"
                                    [ Value.Tuple [] ]))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::TryFrom"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "char" ]
          (* Instance *)
          [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
    End Impl_core_convert_TryFrom_char_for_u16.
    
    Module Impl_core_convert_From_u8_for_char.
      Definition Self : Ty.t := Ty.path "char".
      
      (*
          fn from(i: u8) -> Self {
              i as char
          }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ i ] =>
          ltac:(M.monadic
            (let i := M.alloc (| i |) in
            M.rust_cast (M.read (| i |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "u8" ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_u8_for_char.
    
    (* StructRecord
      {
        name := "ParseCharError";
        const_params := [];
        ty_params := [];
        fields := [ ("kind", Ty.path "core::char::convert::CharErrorKind") ];
      } *)
    
    Module Impl_core_clone_Clone_for_core_char_convert_ParseCharError.
      Definition Self : Ty.t := Ty.path "core::char::convert::ParseCharError".
      
      (* 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::convert::ParseCharError"
              [
                ("kind",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "core::char::convert::CharErrorKind",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "core::char::convert::ParseCharError",
                        "kind"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => 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_convert_ParseCharError.
    
    Module Impl_core_fmt_Debug_for_core_char_convert_ParseCharError.
      Definition Self : Ty.t := Ty.path "core::char::convert::ParseCharError".
      
      (* 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 "ParseCharError" |);
                M.read (| Value.String "kind" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "core::char::convert::ParseCharError",
                    "kind"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_convert_ParseCharError.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_char_convert_ParseCharError.
      Definition Self : Ty.t := Ty.path "core::char::convert::ParseCharError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_char_convert_ParseCharError.
    
    Module Impl_core_cmp_PartialEq_for_core_char_convert_ParseCharError.
      Definition Self : Ty.t := Ty.path "core::char::convert::ParseCharError".
      
      (* 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
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.path "core::char::convert::CharErrorKind",
                [ Ty.path "core::char::convert::CharErrorKind" ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::char::convert::ParseCharError",
                  "kind"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "core::char::convert::ParseCharError",
                  "kind"
                |)
              ]
            |)))
        | _, _, _ => 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_convert_ParseCharError.
    
    Module Impl_core_cmp_Eq_for_core_char_convert_ParseCharError.
      Definition Self : Ty.t := Ty.path "core::char::convert::ParseCharError".
      
      (* 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_convert_ParseCharError.
    
    (*
    Enum CharErrorKind
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "EmptyString";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "TooManyChars";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_marker_Copy_for_core_char_convert_CharErrorKind.
      Definition Self : Ty.t := Ty.path "core::char::convert::CharErrorKind".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_char_convert_CharErrorKind.
    
    Module Impl_core_clone_Clone_for_core_char_convert_CharErrorKind.
      Definition Self : Ty.t := Ty.path "core::char::convert::CharErrorKind".
      
      (* 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.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_char_convert_CharErrorKind.
    
    Module Impl_core_fmt_Debug_for_core_char_convert_CharErrorKind.
      Definition Self : Ty.t := Ty.path "core::char::convert::CharErrorKind".
      
      (* 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", "write_str", [] |),
              [
                M.read (| f |);
                M.read (|
                  M.match_operator (|
                    self,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "core::char::convert::CharErrorKind::EmptyString"
                            |) in
                          M.alloc (| M.read (| Value.String "EmptyString" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "core::char::convert::CharErrorKind::TooManyChars"
                            |) in
                          M.alloc (| M.read (| Value.String "TooManyChars" |) |)))
                    ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_convert_CharErrorKind.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_char_convert_CharErrorKind.
      Definition Self : Ty.t := Ty.path "core::char::convert::CharErrorKind".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_char_convert_CharErrorKind.
    
    Module Impl_core_cmp_PartialEq_for_core_char_convert_CharErrorKind.
      Definition Self : Ty.t := Ty.path "core::char::convert::CharErrorKind".
      
      (* 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
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::char::convert::CharErrorKind" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::char::convert::CharErrorKind" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
            |)))
        | _, _, _ => 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_convert_CharErrorKind.
    
    Module Impl_core_cmp_Eq_for_core_char_convert_CharErrorKind.
      Definition Self : Ty.t := Ty.path "core::char::convert::CharErrorKind".
      
      (* 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
            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_convert_CharErrorKind.
    
    Module Impl_core_error_Error_for_core_char_convert_ParseCharError.
      Definition Self : Ty.t := Ty.path "core::char::convert::ParseCharError".
      
      (*
          fn description(&self) -> &str {
              match self.kind {
                  CharErrorKind::EmptyString => "cannot parse char from empty string",
                  CharErrorKind::TooManyChars => "too many characters in string",
              }
          }
      *)
      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 (|
              M.match_operator (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::char::convert::ParseCharError",
                  "kind"
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "core::char::convert::CharErrorKind::EmptyString"
                        |) in
                      M.alloc (|
                        M.read (| Value.String "cannot parse char from empty string" |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "core::char::convert::CharErrorKind::TooManyChars"
                        |) in
                      M.alloc (| M.read (| Value.String "too many characters in string" |) |)))
                ]
              |)
            |)))
        | _, _, _ => 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_convert_ParseCharError.
    
    Module Impl_core_fmt_Display_for_core_char_convert_ParseCharError.
      Definition Self : Ty.t := Ty.path "core::char::convert::ParseCharError".
      
      (*
          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::char::convert::ParseCharError",
                    [],
                    "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_char_convert_ParseCharError.
    
    Module Impl_core_str_traits_FromStr_for_char.
      Definition Self : Ty.t := Ty.path "char".
      
      (*     type Err = ParseCharError; *)
      Definition _Err : Ty.t := Ty.path "core::char::convert::ParseCharError".
      
      (*
          fn from_str(s: &str) -> Result<Self, Self::Err> {
              let mut chars = s.chars();
              match (chars.next(), chars.next()) {
                  (None, _) => Err(ParseCharError { kind: CharErrorKind::EmptyString }),
                  (Some(c), None) => Ok(c),
                  _ => Err(ParseCharError { kind: CharErrorKind::TooManyChars }),
              }
          }
      *)
      Definition from_str (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ s ] =>
          ltac:(M.monadic
            (let s := M.alloc (| s |) in
            M.read (|
              let~ chars :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "str", "chars", [] |),
                    [ M.read (| s |) ]
                  |)
                |) in
              M.match_operator (|
                M.alloc (|
                  Value.Tuple
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::iterator::Iterator",
                          Ty.path "core::str::iter::Chars",
                          [],
                          "next",
                          []
                        |),
                        [ chars ]
                      |);
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::iterator::Iterator",
                          Ty.path "core::str::iter::Chars",
                          [],
                          "next",
                          []
                        |),
                        [ chars ]
                      |)
                    ]
                |),
                [
                  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 _ := M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [
                            Value.StructRecord
                              "core::char::convert::ParseCharError"
                              [
                                ("kind",
                                  Value.StructTuple
                                    "core::char::convert::CharErrorKind::EmptyString"
                                    [])
                              ]
                          ]
                      |)));
                  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 γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ0_0,
                          "core::option::Option::Some",
                          0
                        |) in
                      let c := M.copy (| γ1_0 |) in
                      let _ := M.is_struct_tuple (| γ0_1, "core::option::Option::None" |) in
                      M.alloc (|
                        Value.StructTuple "core::result::Result::Ok" [ M.read (| c |) ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [
                            Value.StructRecord
                              "core::char::convert::ParseCharError"
                              [
                                ("kind",
                                  Value.StructTuple
                                    "core::char::convert::CharErrorKind::TooManyChars"
                                    [])
                              ]
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::str::traits::FromStr"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Err", InstanceField.Ty _Err); ("from_str", InstanceField.Method from_str) ].
    End Impl_core_str_traits_FromStr_for_char.
    
    (*
    const fn char_try_from_u32(i: u32) -> Result<char, CharTryFromError> {
        // This is an optimized version of the check
        // (i > MAX as u32) || (i >= 0xD800 && i <= 0xDFFF),
        // which can also be written as
        // i >= 0x110000 || (i >= 0xD800 && i < 0xE000).
        //
        // The XOR with 0xD800 permutes the ranges such that 0xD800..0xE000 is
        // mapped to 0x0000..0x0800, while keeping all the high bits outside 0xFFFF the same.
        // In particular, numbers >= 0x110000 stay in this range.
        //
        // Subtracting 0x800 causes 0x0000..0x0800 to wrap, meaning that a single
        // unsigned comparison against 0x110000 - 0x800 will detect both the wrapped
        // surrogate range as well as the numbers originally larger than 0x110000.
        //
        if (i ^ 0xD800).wrapping_sub(0x800) >= 0x110000 - 0x800 {
            Err(CharTryFromError(()))
        } else {
            // SAFETY: checked that it's a legal unicode value
            Ok(unsafe { transmute(i) })
        }
    }
    *)
    Definition char_try_from_u32 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ i ] =>
        ltac:(M.monadic
          (let i := M.alloc (| i |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          BinOp.ge (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "u32", "wrapping_sub", [] |),
                              [
                                BinOp.bit_xor
                                  (M.read (| i |))
                                  (Value.Integer IntegerKind.U32 55296);
                                Value.Integer IntegerKind.U32 2048
                              ]
                            |),
                            BinOp.Wrap.sub (|
                              Value.Integer IntegerKind.U32 1114112,
                              Value.Integer IntegerKind.U32 2048
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [
                          Value.StructTuple
                            "core::char::convert::CharTryFromError"
                            [ Value.Tuple [] ]
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          M.call_closure (|
                            M.get_function (|
                              "core::intrinsics::transmute",
                              [ Ty.path "u32"; Ty.path "char" ]
                            |),
                            [ M.read (| i |) ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_char_try_from_u32 :
      M.IsFunction "core::char::convert::char_try_from_u32" char_try_from_u32.
    
    Module Impl_core_convert_TryFrom_u32_for_char.
      Definition Self : Ty.t := Ty.path "char".
      
      (*     type Error = CharTryFromError; *)
      Definition _Error : Ty.t := Ty.path "core::char::convert::CharTryFromError".
      
      (*
          fn try_from(i: u32) -> Result<Self, Self::Error> {
              char_try_from_u32(i)
          }
      *)
      Definition try_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ i ] =>
          ltac:(M.monadic
            (let i := M.alloc (| i |) in
            M.call_closure (|
              M.get_function (| "core::char::convert::char_try_from_u32", [] |),
              [ M.read (| i |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::TryFrom"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "u32" ]
          (* Instance *)
          [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
    End Impl_core_convert_TryFrom_u32_for_char.
    
    (* StructTuple
      {
        name := "CharTryFromError";
        const_params := [];
        ty_params := [];
        fields := [ Ty.tuple [] ];
      } *)
    
    Module Impl_core_marker_Copy_for_core_char_convert_CharTryFromError.
      Definition Self : Ty.t := Ty.path "core::char::convert::CharTryFromError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_char_convert_CharTryFromError.
    
    Module Impl_core_clone_Clone_for_core_char_convert_CharTryFromError.
      Definition Self : Ty.t := Ty.path "core::char::convert::CharTryFromError".
      
      (* 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_char_convert_CharTryFromError.
    
    Module Impl_core_fmt_Debug_for_core_char_convert_CharTryFromError.
      Definition Self : Ty.t := Ty.path "core::char::convert::CharTryFromError".
      
      (* 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 "CharTryFromError" |);
                M.alloc (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "core::char::convert::CharTryFromError",
                    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_char_convert_CharTryFromError.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_char_convert_CharTryFromError.
      Definition Self : Ty.t := Ty.path "core::char::convert::CharTryFromError".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_char_convert_CharTryFromError.
    
    Module Impl_core_cmp_PartialEq_for_core_char_convert_CharTryFromError.
      Definition Self : Ty.t := Ty.path "core::char::convert::CharTryFromError".
      
      (* 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
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.tuple [],
                [ Ty.tuple [] ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "core::char::convert::CharTryFromError",
                  0
                |);
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| other |),
                  "core::char::convert::CharTryFromError",
                  0
                |)
              ]
            |)))
        | _, _, _ => 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_convert_CharTryFromError.
    
    Module Impl_core_cmp_Eq_for_core_char_convert_CharTryFromError.
      Definition Self : Ty.t := Ty.path "core::char::convert::CharTryFromError".
      
      (* 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_convert_CharTryFromError.
    
    Module Impl_core_fmt_Display_for_core_char_convert_CharTryFromError.
      Definition Self : Ty.t := Ty.path "core::char::convert::CharTryFromError".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              "converted integer out of range for `char`".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.read (| Value.String "converted integer out of range for `char`" |);
                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_char_convert_CharTryFromError.
    
    (*
    pub(super) const fn from_digit(num: u32, radix: u32) -> Option<char> {
        if radix > 36 {
            panic!("from_digit: radix is too high (maximum 36)");
        }
        if num < radix {
            let num = num as u8;
            if num < 10 { Some((b'0' + num) as char) } else { Some((b'a' + num - 10) as char) }
        } else {
            None
        }
    }
    *)
    Definition from_digit (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ num; radix ] =>
        ltac:(M.monadic
          (let num := M.alloc (| num |) in
          let radix := M.alloc (| radix |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.gt (| M.read (| radix |), Value.Integer IntegerKind.U32 36 |)
                          |)) 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_fmt", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_const",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.read (|
                                          Value.String "from_digit: radix is too high (maximum 36)"
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use (M.alloc (| BinOp.lt (| M.read (| num |), M.read (| radix |) |) |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    let~ num := M.alloc (| M.rust_cast (M.read (| num |)) |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.lt (| M.read (| num |), Value.Integer IntegerKind.U8 10 |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              Value.StructTuple
                                "core::option::Option::Some"
                                [
                                  M.rust_cast
                                    (BinOp.Wrap.add (|
                                      M.read (| UnsupportedLiteral |),
                                      M.read (| num |)
                                    |))
                                ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              Value.StructTuple
                                "core::option::Option::Some"
                                [
                                  M.rust_cast
                                    (BinOp.Wrap.sub (|
                                      BinOp.Wrap.add (|
                                        M.read (| UnsupportedLiteral |),
                                        M.read (| num |)
                                      |),
                                      Value.Integer IntegerKind.U8 10
                                    |))
                                ]
                            |)))
                      ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_from_digit : M.IsFunction "core::char::convert::from_digit" from_digit.
  End convert.
End char.
