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

Module char.
  Module methods.
    Module Impl_char.
      Definition Self : Ty.t := Ty.path "char".
      
      (*     pub const MIN: char = '\0'; *)
      (* Ty.path "char" *)
      Definition value_MIN : Value.t := M.run ltac:(M.monadic (M.alloc (| Value.UnicodeChar 0 |))).
      
      Axiom AssociatedConstant_value_MIN : M.IsAssociatedConstant Self "value_MIN" value_MIN.
      
      (*     pub const MAX: char = '\u{10ffff}'; *)
      (* Ty.path "char" *)
      Definition value_MAX : Value.t :=
        M.run ltac:(M.monadic (M.alloc (| Value.UnicodeChar 1114111 |))).
      
      Axiom AssociatedConstant_value_MAX : M.IsAssociatedConstant Self "value_MAX" value_MAX.
      
      (*     pub const REPLACEMENT_CHARACTER: char = '\u{FFFD}'; *)
      (* Ty.path "char" *)
      Definition value_REPLACEMENT_CHARACTER : Value.t :=
        M.run ltac:(M.monadic (M.alloc (| Value.UnicodeChar 65533 |))).
      
      Axiom AssociatedConstant_value_REPLACEMENT_CHARACTER :
        M.IsAssociatedConstant Self "value_REPLACEMENT_CHARACTER" value_REPLACEMENT_CHARACTER.
      
      (*     pub const UNICODE_VERSION: (u8, u8, u8) = crate::unicode::UNICODE_VERSION; *)
      (* Ty.tuple [ Ty.path "u8"; Ty.path "u8"; Ty.path "u8" ] *)
      Definition value_UNICODE_VERSION : Value.t :=
        M.run ltac:(M.monadic (M.get_constant (| "core::unicode::UNICODE_VERSION" |))).
      
      Axiom AssociatedConstant_value_UNICODE_VERSION :
        M.IsAssociatedConstant Self "value_UNICODE_VERSION" value_UNICODE_VERSION.
      
      (*
          pub fn decode_utf16<I: IntoIterator<Item = u16>>(iter: I) -> DecodeUtf16<I::IntoIter> {
              super::decode::decode_utf16(iter)
          }
      *)
      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
            M.call_closure (|
              M.get_function (| "core::char::decode::decode_utf16", [ I ] |),
              [ M.read (| iter |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_decode_utf16 :
        M.IsAssociatedFunction Self "decode_utf16" decode_utf16.
      
      (*
          pub const fn from_u32(i: u32) -> Option<char> {
              super::convert::from_u32(i)
          }
      *)
      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.call_closure (|
              M.get_function (| "core::char::convert::from_u32", [] |),
              [ M.read (| i |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_u32 : M.IsAssociatedFunction Self "from_u32" from_u32.
      
      (*
          pub const unsafe fn from_u32_unchecked(i: u32) -> char {
              // SAFETY: the safety contract must be upheld by the caller.
              unsafe { super::convert::from_u32_unchecked(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.call_closure (|
              M.get_function (| "core::char::convert::from_u32_unchecked", [] |),
              [ M.read (| i |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_u32_unchecked :
        M.IsAssociatedFunction Self "from_u32_unchecked" from_u32_unchecked.
      
      (*
          pub const fn from_digit(num: u32, radix: u32) -> Option<char> {
              super::convert::from_digit(num, radix)
          }
      *)
      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.call_closure (|
              M.get_function (| "core::char::convert::from_digit", [] |),
              [ M.read (| num |); M.read (| radix |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_digit : M.IsAssociatedFunction Self "from_digit" from_digit.
      
      (*
          pub fn is_digit(self, radix: u32) -> bool {
              self.to_digit(radix).is_some()
          }
      *)
      Definition is_digit (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; radix ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let radix := M.alloc (| radix |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u32" ],
                "is_some",
                []
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "char", "to_digit", [] |),
                    [ M.read (| self |); M.read (| radix |) ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_digit : M.IsAssociatedFunction Self "is_digit" is_digit.
      
      (*
          pub const fn to_digit(self, radix: u32) -> Option<u32> {
              // If not a digit, a number greater than radix will be created.
              let mut digit = (self as u32).wrapping_sub('0' as u32);
              if radix > 10 {
                  assert!(radix <= 36, "to_digit: radix is too high (maximum 36)");
                  if digit < 10 {
                      return Some(digit);
                  }
                  // Force the 6th bit to be set to ensure ascii is lower case.
                  digit = (self as u32 | 0b10_0000).wrapping_sub('a' as u32).saturating_add(10);
              }
              // FIXME(const-hack): once then_some is const fn, use it here
              if digit < radix { Some(digit) } else { None }
          }
      *)
      Definition to_digit (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; radix ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let radix := M.alloc (| radix |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ digit :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "u32", "wrapping_sub", [] |),
                        [ M.rust_cast (M.read (| self |)); M.rust_cast (Value.UnicodeChar 48) ]
                      |)
                    |) in
                  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 10
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            UnOp.not (|
                                              BinOp.le (|
                                                M.read (| 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
                                                            "to_digit: radix is too high (maximum 36)"
                                                        |)
                                                      ]
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            BinOp.lt (|
                                              M.read (| digit |),
                                              Value.Integer IntegerKind.U32 10
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            M.return_ (|
                                              Value.StructTuple
                                                "core::option::Option::Some"
                                                [ M.read (| digit |) ]
                                            |)
                                          |)
                                        |)
                                      |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            let~ _ :=
                              M.write (|
                                digit,
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "u32",
                                    "saturating_add",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "u32",
                                        "wrapping_sub",
                                        []
                                      |),
                                      [
                                        BinOp.bit_or
                                          (M.rust_cast (M.read (| self |)))
                                          (Value.Integer IntegerKind.U32 32);
                                        M.rust_cast (Value.UnicodeChar 97)
                                      ]
                                    |);
                                    Value.Integer IntegerKind.U32 10
                                  ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        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 (| digit |), M.read (| radix |) |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            Value.StructTuple "core::option::Option::Some" [ M.read (| digit |) ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_to_digit : M.IsAssociatedFunction Self "to_digit" to_digit.
      
      (*
          pub fn escape_unicode(self) -> EscapeUnicode {
              EscapeUnicode::new(self)
          }
      *)
      Definition escape_unicode (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::char::EscapeUnicode", "new", [] |),
              [ M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_escape_unicode :
        M.IsAssociatedFunction Self "escape_unicode" escape_unicode.
      
      (*
          pub(crate) fn escape_debug_ext(self, args: EscapeDebugExtArgs) -> EscapeDebug {
              match self {
                  '\0' => EscapeDebug::backslash(ascii::Char::Digit0),
                  '\t' => EscapeDebug::backslash(ascii::Char::SmallT),
                  '\r' => EscapeDebug::backslash(ascii::Char::SmallR),
                  '\n' => EscapeDebug::backslash(ascii::Char::SmallN),
                  '\\' => EscapeDebug::backslash(ascii::Char::ReverseSolidus),
                  '\"' if args.escape_double_quote => EscapeDebug::backslash(ascii::Char::QuotationMark),
                  '\'' if args.escape_single_quote => EscapeDebug::backslash(ascii::Char::Apostrophe),
                  _ if args.escape_grapheme_extended && self.is_grapheme_extended() => {
                      EscapeDebug::unicode(self)
                  }
                  _ if is_printable(self) => EscapeDebug::printable(self),
                  _ => EscapeDebug::unicode(self),
              }
          }
      "
      *)
      Definition escape_debug_ext (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; args ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let args := M.alloc (| args |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (| M.read (| γ |), Value.UnicodeChar 0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDebug",
                            "backslash",
                            []
                          |),
                          [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::Digit0" [] ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (| M.read (| γ |), Value.UnicodeChar 9 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDebug",
                            "backslash",
                            []
                          |),
                          [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallT" [] ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (| M.read (| γ |), Value.UnicodeChar 13 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDebug",
                            "backslash",
                            []
                          |),
                          [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallR" [] ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (| M.read (| γ |), Value.UnicodeChar 10 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDebug",
                            "backslash",
                            []
                          |),
                          [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallN" [] ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (| M.read (| γ |), Value.UnicodeChar 92 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDebug",
                            "backslash",
                            []
                          |),
                          [
                            Value.StructTuple
                              "core::ascii::ascii_char::AsciiChar::ReverseSolidus"
                              []
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (| M.read (| γ |), Value.UnicodeChar 34 |) in
                      let γ :=
                        M.SubPointer.get_struct_record_field (|
                          args,
                          "core::char::methods::EscapeDebugExtArgs",
                          "escape_double_quote"
                        |) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDebug",
                            "backslash",
                            []
                          |),
                          [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::QuotationMark" []
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (| M.read (| γ |), Value.UnicodeChar 39 |) in
                      let γ :=
                        M.SubPointer.get_struct_record_field (|
                          args,
                          "core::char::methods::EscapeDebugExtArgs",
                          "escape_single_quote"
                        |) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDebug",
                            "backslash",
                            []
                          |),
                          [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::Apostrophe" [] ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.SubPointer.get_struct_record_field (|
                          args,
                          "core::char::methods::EscapeDebugExtArgs",
                          "escape_grapheme_extended"
                        |) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let γ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "char",
                              "is_grapheme_extended",
                              []
                            |),
                            [ M.read (| self |) ]
                          |)
                        |) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDebug",
                            "unicode",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (| "core::unicode::printable::is_printable", [] |),
                            [ M.read (| self |) ]
                          |)
                        |) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDebug",
                            "printable",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDebug",
                            "unicode",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_escape_debug_ext :
        M.IsAssociatedFunction Self "escape_debug_ext" escape_debug_ext.
      
      (*
          pub fn escape_debug(self) -> EscapeDebug {
              self.escape_debug_ext(EscapeDebugExtArgs::ESCAPE_ALL)
          }
      *)
      Definition escape_debug (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "char", "escape_debug_ext", [] |),
              [
                M.read (| self |);
                M.read (| M.get_constant (| "core::char::methods::ESCAPE_ALL" |) |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_escape_debug :
        M.IsAssociatedFunction Self "escape_debug" escape_debug.
      
      (*
          pub fn escape_default(self) -> EscapeDefault {
              match self {
                  '\t' => EscapeDefault::backslash(ascii::Char::SmallT),
                  '\r' => EscapeDefault::backslash(ascii::Char::SmallR),
                  '\n' => EscapeDefault::backslash(ascii::Char::SmallN),
                  '\\' | '\'' | '\"' => EscapeDefault::backslash(self.as_ascii().unwrap()),
                  '\x20'..='\x7e' => EscapeDefault::printable(self.as_ascii().unwrap()),
                  _ => EscapeDefault::unicode(self),
              }
          }
      "
      *)
      Definition escape_default (ε : 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 (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (| M.read (| γ |), Value.UnicodeChar 9 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDefault",
                            "backslash",
                            []
                          |),
                          [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallT" [] ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (| M.read (| γ |), Value.UnicodeChar 13 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDefault",
                            "backslash",
                            []
                          |),
                          [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallR" [] ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_constant_or_break_match (| M.read (| γ |), Value.UnicodeChar 10 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDefault",
                            "backslash",
                            []
                          |),
                          [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallN" [] ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.find_or_pattern (|
                        γ,
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.UnicodeChar 92
                                |) in
                              Value.Tuple []));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.UnicodeChar 39
                                |) in
                              Value.Tuple []));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.UnicodeChar 34
                                |) in
                              Value.Tuple []))
                        ],
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [] =>
                                ltac:(M.monadic
                                  (M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::char::EscapeDefault",
                                        "backslash",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "core::ascii::ascii_char::AsciiChar" ],
                                            "unwrap",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "char",
                                                "as_ascii",
                                                []
                                              |),
                                              [ self ]
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDefault",
                            "printable",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.path "core::ascii::ascii_char::AsciiChar" ],
                                "unwrap",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (| Ty.path "char", "as_ascii", [] |),
                                  [ self ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::char::EscapeDefault",
                            "unicode",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_escape_default :
        M.IsAssociatedFunction Self "escape_default" escape_default.
      
      (*
          pub const fn len_utf8(self) -> usize {
              len_utf8(self as u32)
          }
      *)
      Definition len_utf8 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (| "core::char::methods::len_utf8", [] |),
              [ M.rust_cast (M.read (| self |)) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_len_utf8 : M.IsAssociatedFunction Self "len_utf8" len_utf8.
      
      (*
          pub const fn len_utf16(self) -> usize {
              len_utf16(self as u32)
          }
      *)
      Definition len_utf16 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (| "core::char::methods::len_utf16", [] |),
              [ M.rust_cast (M.read (| self |)) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_len_utf16 : M.IsAssociatedFunction Self "len_utf16" len_utf16.
      
      (*
          pub const fn encode_utf8(self, dst: &mut [u8]) -> &mut str {
              // SAFETY: `char` is not a surrogate, so this is valid UTF-8.
              unsafe { from_utf8_unchecked_mut(encode_utf8_raw(self as u32, dst)) }
          }
      *)
      Definition encode_utf8 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; dst ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let dst := M.alloc (| dst |) in
            M.call_closure (|
              M.get_function (| "core::str::converts::from_utf8_unchecked_mut", [] |),
              [
                M.call_closure (|
                  M.get_function (| "core::char::methods::encode_utf8_raw", [] |),
                  [ M.rust_cast (M.read (| self |)); M.read (| dst |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_encode_utf8 : M.IsAssociatedFunction Self "encode_utf8" encode_utf8.
      
      (*
          pub const fn encode_utf16(self, dst: &mut [u16]) -> &mut [u16] {
              encode_utf16_raw(self as u32, dst)
          }
      *)
      Definition encode_utf16 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; dst ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let dst := M.alloc (| dst |) in
            M.call_closure (|
              M.get_function (| "core::char::methods::encode_utf16_raw", [] |),
              [ M.rust_cast (M.read (| self |)); M.read (| dst |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_encode_utf16 :
        M.IsAssociatedFunction Self "encode_utf16" encode_utf16.
      
      (*
          pub fn is_alphabetic(self) -> bool {
              match self {
                  'a'..='z' | 'A'..='Z' => true,
                  c => c > '\x7f' && unicode::Alphabetic(c),
              }
          }
      *)
      Definition is_alphabetic (ε : 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 (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (M.find_or_pattern (|
                        γ,
                        [
                          fun γ => ltac:(M.monadic (Value.Tuple []));
                          fun γ => ltac:(M.monadic (Value.Tuple []))
                        ],
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let c := M.copy (| γ |) in
                      M.alloc (|
                        LogicalOp.and (|
                          BinOp.gt (| M.read (| c |), Value.UnicodeChar 127 |),
                          ltac:(M.monadic
                            (M.call_closure (|
                              M.get_function (|
                                "core::unicode::unicode_data::alphabetic::lookup",
                                []
                              |),
                              [ M.read (| c |) ]
                            |)))
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_alphabetic :
        M.IsAssociatedFunction Self "is_alphabetic" is_alphabetic.
      
      (*
          pub const fn is_lowercase(self) -> bool {
              match self {
                  'a'..='z' => true,
                  c => c > '\x7f' && unicode::Lowercase(c),
              }
          }
      *)
      Definition is_lowercase (ε : 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 (|
                self,
                [
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let c := M.copy (| γ |) in
                      M.alloc (|
                        LogicalOp.and (|
                          BinOp.gt (| M.read (| c |), Value.UnicodeChar 127 |),
                          ltac:(M.monadic
                            (M.call_closure (|
                              M.get_function (|
                                "core::unicode::unicode_data::lowercase::lookup",
                                []
                              |),
                              [ M.read (| c |) ]
                            |)))
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_lowercase :
        M.IsAssociatedFunction Self "is_lowercase" is_lowercase.
      
      (*
          pub const fn is_uppercase(self) -> bool {
              match self {
                  'A'..='Z' => true,
                  c => c > '\x7f' && unicode::Uppercase(c),
              }
          }
      *)
      Definition is_uppercase (ε : 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 (|
                self,
                [
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let c := M.copy (| γ |) in
                      M.alloc (|
                        LogicalOp.and (|
                          BinOp.gt (| M.read (| c |), Value.UnicodeChar 127 |),
                          ltac:(M.monadic
                            (M.call_closure (|
                              M.get_function (|
                                "core::unicode::unicode_data::uppercase::lookup",
                                []
                              |),
                              [ M.read (| c |) ]
                            |)))
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_uppercase :
        M.IsAssociatedFunction Self "is_uppercase" is_uppercase.
      
      (*
          pub fn is_whitespace(self) -> bool {
              match self {
                  ' ' | '\x09'..='\x0d' => true,
                  c => c > '\x7f' && unicode::White_Space(c),
              }
          }
      *)
      Definition is_whitespace (ε : 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 (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (M.find_or_pattern (|
                        γ,
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.UnicodeChar 32
                                |) in
                              Value.Tuple []));
                          fun γ => ltac:(M.monadic (Value.Tuple []))
                        ],
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let c := M.copy (| γ |) in
                      M.alloc (|
                        LogicalOp.and (|
                          BinOp.gt (| M.read (| c |), Value.UnicodeChar 127 |),
                          ltac:(M.monadic
                            (M.call_closure (|
                              M.get_function (|
                                "core::unicode::unicode_data::white_space::lookup",
                                []
                              |),
                              [ M.read (| c |) ]
                            |)))
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_whitespace :
        M.IsAssociatedFunction Self "is_whitespace" is_whitespace.
      
      (*
          pub fn is_alphanumeric(self) -> bool {
              self.is_alphabetic() || self.is_numeric()
          }
      *)
      Definition is_alphanumeric (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            LogicalOp.or (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "char", "is_alphabetic", [] |),
                [ M.read (| self |) ]
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_associated_function (| Ty.path "char", "is_numeric", [] |),
                  [ M.read (| self |) ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_alphanumeric :
        M.IsAssociatedFunction Self "is_alphanumeric" is_alphanumeric.
      
      (*
          pub fn is_control(self) -> bool {
              unicode::Cc(self)
          }
      *)
      Definition is_control (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (| "core::unicode::unicode_data::cc::lookup", [] |),
              [ M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_control : M.IsAssociatedFunction Self "is_control" is_control.
      
      (*
          pub(crate) fn is_grapheme_extended(self) -> bool {
              unicode::Grapheme_Extend(self)
          }
      *)
      Definition is_grapheme_extended (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_function (| "core::unicode::unicode_data::grapheme_extend::lookup", [] |),
              [ M.read (| self |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_grapheme_extended :
        M.IsAssociatedFunction Self "is_grapheme_extended" is_grapheme_extended.
      
      (*
          pub fn is_numeric(self) -> bool {
              match self {
                  '0'..='9' => true,
                  c => c > '\x7f' && unicode::N(c),
              }
          }
      *)
      Definition is_numeric (ε : 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 (|
                self,
                [
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let c := M.copy (| γ |) in
                      M.alloc (|
                        LogicalOp.and (|
                          BinOp.gt (| M.read (| c |), Value.UnicodeChar 127 |),
                          ltac:(M.monadic
                            (M.call_closure (|
                              M.get_function (| "core::unicode::unicode_data::n::lookup", [] |),
                              [ M.read (| c |) ]
                            |)))
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_numeric : M.IsAssociatedFunction Self "is_numeric" is_numeric.
      
      (*
          pub fn to_lowercase(self) -> ToLowercase {
              ToLowercase(CaseMappingIter::new(conversions::to_lower(self)))
          }
      *)
      Definition to_lowercase (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructTuple
              "core::char::ToLowercase"
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::char::CaseMappingIter", "new", [] |),
                  [
                    M.call_closure (|
                      M.get_function (| "core::unicode::unicode_data::conversions::to_lower", [] |),
                      [ M.read (| self |) ]
                    |)
                  ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_to_lowercase :
        M.IsAssociatedFunction Self "to_lowercase" to_lowercase.
      
      (*
          pub fn to_uppercase(self) -> ToUppercase {
              ToUppercase(CaseMappingIter::new(conversions::to_upper(self)))
          }
      *)
      Definition to_uppercase (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructTuple
              "core::char::ToUppercase"
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::char::CaseMappingIter", "new", [] |),
                  [
                    M.call_closure (|
                      M.get_function (| "core::unicode::unicode_data::conversions::to_upper", [] |),
                      [ M.read (| self |) ]
                    |)
                  ]
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_to_uppercase :
        M.IsAssociatedFunction Self "to_uppercase" to_uppercase.
      
      (*
          pub const fn is_ascii(&self) -> bool {
              *self as u32 <= 0x7F
          }
      *)
      Definition is_ascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            BinOp.le (|
              M.rust_cast (M.read (| M.read (| self |) |)),
              Value.Integer IntegerKind.U32 127
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_ascii : M.IsAssociatedFunction Self "is_ascii" is_ascii.
      
      (*
          pub const fn as_ascii(&self) -> Option<ascii::Char> {
              if self.is_ascii() {
                  // SAFETY: Just checked that this is ASCII.
                  Some(unsafe { ascii::Char::from_u8_unchecked( *self as u8) })
              } else {
                  None
              }
          }
      *)
      Definition as_ascii (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "char", "is_ascii", [] |),
                              [ M.read (| self |) ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ascii::ascii_char::AsciiChar",
                                "from_u8_unchecked",
                                []
                              |),
                              [ M.rust_cast (M.read (| M.read (| self |) |)) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_ascii : M.IsAssociatedFunction Self "as_ascii" as_ascii.
      
      (*
          pub const fn to_ascii_uppercase(&self) -> char {
              if self.is_ascii_lowercase() {
                  ( *self as u8).ascii_change_case_unchecked() as char
              } else {
                  *self
              }
          }
      *)
      Definition to_ascii_uppercase (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "char",
                                "is_ascii_lowercase",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.rust_cast
                          (M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "u8",
                              "ascii_change_case_unchecked",
                              []
                            |),
                            [ M.alloc (| M.rust_cast (M.read (| M.read (| self |) |)) |) ]
                          |))
                      |)));
                  fun γ => ltac:(M.monadic (M.read (| self |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_to_ascii_uppercase :
        M.IsAssociatedFunction Self "to_ascii_uppercase" to_ascii_uppercase.
      
      (*
          pub const fn to_ascii_lowercase(&self) -> char {
              if self.is_ascii_uppercase() {
                  ( *self as u8).ascii_change_case_unchecked() as char
              } else {
                  *self
              }
          }
      *)
      Definition to_ascii_lowercase (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "char",
                                "is_ascii_uppercase",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.rust_cast
                          (M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "u8",
                              "ascii_change_case_unchecked",
                              []
                            |),
                            [ M.alloc (| M.rust_cast (M.read (| M.read (| self |) |)) |) ]
                          |))
                      |)));
                  fun γ => ltac:(M.monadic (M.read (| self |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_to_ascii_lowercase :
        M.IsAssociatedFunction Self "to_ascii_lowercase" to_ascii_lowercase.
      
      (*
          pub const fn eq_ignore_ascii_case(&self, other: &char) -> bool {
              self.to_ascii_lowercase() == other.to_ascii_lowercase()
          }
      *)
      Definition eq_ignore_ascii_case (ε : 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.call_closure (|
                M.get_associated_function (| Ty.path "char", "to_ascii_lowercase", [] |),
                [ M.read (| self |) ]
              |),
              M.call_closure (|
                M.get_associated_function (| Ty.path "char", "to_ascii_lowercase", [] |),
                [ M.read (| other |) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_eq_ignore_ascii_case :
        M.IsAssociatedFunction Self "eq_ignore_ascii_case" eq_ignore_ascii_case.
      
      (*
          pub const fn make_ascii_uppercase(&mut self) {
              *self = self.to_ascii_uppercase();
          }
      *)
      Definition make_ascii_uppercase (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ _ :=
                M.write (|
                  M.read (| self |),
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "char", "to_ascii_uppercase", [] |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_make_ascii_uppercase :
        M.IsAssociatedFunction Self "make_ascii_uppercase" make_ascii_uppercase.
      
      (*
          pub const fn make_ascii_lowercase(&mut self) {
              *self = self.to_ascii_lowercase();
          }
      *)
      Definition make_ascii_lowercase (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ _ :=
                M.write (|
                  M.read (| self |),
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "char", "to_ascii_lowercase", [] |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_make_ascii_lowercase :
        M.IsAssociatedFunction Self "make_ascii_lowercase" make_ascii_lowercase.
      
      (*
          pub const fn is_ascii_alphabetic(&self) -> bool {
              matches!( *self, 'A'..='Z' | 'a'..='z')
          }
      *)
      Definition is_ascii_alphabetic (ε : 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.read (| self |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (M.find_or_pattern (|
                        γ,
                        [
                          fun γ => ltac:(M.monadic (Value.Tuple []));
                          fun γ => ltac:(M.monadic (Value.Tuple []))
                        ],
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_ascii_alphabetic :
        M.IsAssociatedFunction Self "is_ascii_alphabetic" is_ascii_alphabetic.
      
      (*
          pub const fn is_ascii_uppercase(&self) -> bool {
              matches!( *self, 'A'..='Z')
          }
      *)
      Definition is_ascii_uppercase (ε : 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.read (| self |),
                [
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_ascii_uppercase :
        M.IsAssociatedFunction Self "is_ascii_uppercase" is_ascii_uppercase.
      
      (*
          pub const fn is_ascii_lowercase(&self) -> bool {
              matches!( *self, 'a'..='z')
          }
      *)
      Definition is_ascii_lowercase (ε : 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.read (| self |),
                [
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_ascii_lowercase :
        M.IsAssociatedFunction Self "is_ascii_lowercase" is_ascii_lowercase.
      
      (*
          pub const fn is_ascii_alphanumeric(&self) -> bool {
              matches!( *self, '0'..='9') | matches!( *self, 'A'..='Z') | matches!( *self, 'a'..='z')
          }
      *)
      Definition is_ascii_alphanumeric (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            BinOp.bit_or
              (BinOp.bit_or
                (M.read (|
                  M.match_operator (|
                    M.read (| self |),
                    [
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                    ]
                  |)
                |))
                (M.read (|
                  M.match_operator (|
                    M.read (| self |),
                    [
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                    ]
                  |)
                |)))
              (M.read (|
                M.match_operator (|
                  M.read (| self |),
                  [
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                  ]
                |)
              |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_ascii_alphanumeric :
        M.IsAssociatedFunction Self "is_ascii_alphanumeric" is_ascii_alphanumeric.
      
      (*
          pub const fn is_ascii_digit(&self) -> bool {
              matches!( *self, '0'..='9')
          }
      *)
      Definition is_ascii_digit (ε : 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.read (| self |),
                [
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_ascii_digit :
        M.IsAssociatedFunction Self "is_ascii_digit" is_ascii_digit.
      
      (*
          pub const fn is_ascii_octdigit(&self) -> bool {
              matches!( *self, '0'..='7')
          }
      *)
      Definition is_ascii_octdigit (ε : 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.read (| self |),
                [
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_ascii_octdigit :
        M.IsAssociatedFunction Self "is_ascii_octdigit" is_ascii_octdigit.
      
      (*
          pub const fn is_ascii_hexdigit(&self) -> bool {
              matches!( *self, '0'..='9') | matches!( *self, 'A'..='F') | matches!( *self, 'a'..='f')
          }
      *)
      Definition is_ascii_hexdigit (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            BinOp.bit_or
              (BinOp.bit_or
                (M.read (|
                  M.match_operator (|
                    M.read (| self |),
                    [
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                    ]
                  |)
                |))
                (M.read (|
                  M.match_operator (|
                    M.read (| self |),
                    [
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                    ]
                  |)
                |)))
              (M.read (|
                M.match_operator (|
                  M.read (| self |),
                  [
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                  ]
                |)
              |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_ascii_hexdigit :
        M.IsAssociatedFunction Self "is_ascii_hexdigit" is_ascii_hexdigit.
      
      (*
          pub const fn is_ascii_punctuation(&self) -> bool {
              matches!( *self, '!'..='/')
                  | matches!( *self, ':'..='@')
                  | matches!( *self, '['..='`')
                  | matches!( *self, '{'..='~')
          }
      *)
      Definition is_ascii_punctuation (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            BinOp.bit_or
              (BinOp.bit_or
                (BinOp.bit_or
                  (M.read (|
                    M.match_operator (|
                      M.read (| self |),
                      [
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                      ]
                    |)
                  |))
                  (M.read (|
                    M.match_operator (|
                      M.read (| self |),
                      [
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                      ]
                    |)
                  |)))
                (M.read (|
                  M.match_operator (|
                    M.read (| self |),
                    [
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                    ]
                  |)
                |)))
              (M.read (|
                M.match_operator (|
                  M.read (| self |),
                  [
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                  ]
                |)
              |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_ascii_punctuation :
        M.IsAssociatedFunction Self "is_ascii_punctuation" is_ascii_punctuation.
      
      (*
          pub const fn is_ascii_graphic(&self) -> bool {
              matches!( *self, '!'..='~')
          }
      *)
      Definition is_ascii_graphic (ε : 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.read (| self |),
                [
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_ascii_graphic :
        M.IsAssociatedFunction Self "is_ascii_graphic" is_ascii_graphic.
      
      (*
          pub const fn is_ascii_whitespace(&self) -> bool {
              matches!( *self, '\t' | '\n' | '\x0C' | '\r' | ' ')
          }
      *)
      Definition is_ascii_whitespace (ε : 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.read (| self |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (M.find_or_pattern (|
                        γ,
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.UnicodeChar 9
                                |) in
                              Value.Tuple []));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.UnicodeChar 10
                                |) in
                              Value.Tuple []));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.UnicodeChar 12
                                |) in
                              Value.Tuple []));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.UnicodeChar 13
                                |) in
                              Value.Tuple []));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.UnicodeChar 32
                                |) in
                              Value.Tuple []))
                        ],
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_ascii_whitespace :
        M.IsAssociatedFunction Self "is_ascii_whitespace" is_ascii_whitespace.
      
      (*
          pub const fn is_ascii_control(&self) -> bool {
              matches!( *self, '\0'..='\x1F' | '\x7F')
          }
      *)
      Definition is_ascii_control (ε : 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.read (| self |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (M.find_or_pattern (|
                        γ,
                        [
                          fun γ => ltac:(M.monadic (Value.Tuple []));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.UnicodeChar 127
                                |) in
                              Value.Tuple []))
                        ],
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_ascii_control :
        M.IsAssociatedFunction Self "is_ascii_control" is_ascii_control.
    End Impl_char.
    
    (* StructRecord
      {
        name := "EscapeDebugExtArgs";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("escape_grapheme_extended", Ty.path "bool");
            ("escape_single_quote", Ty.path "bool");
            ("escape_double_quote", Ty.path "bool")
          ];
      } *)
    
    Module Impl_core_char_methods_EscapeDebugExtArgs.
      Definition Self : Ty.t := Ty.path "core::char::methods::EscapeDebugExtArgs".
      
      (*
          pub(crate) const ESCAPE_ALL: Self = Self {
              escape_grapheme_extended: true,
              escape_single_quote: true,
              escape_double_quote: true,
          };
      *)
      (* Ty.path "core::char::methods::EscapeDebugExtArgs" *)
      Definition value_ESCAPE_ALL : Value.t :=
        M.run
          ltac:(M.monadic
            (M.alloc (|
              Value.StructRecord
                "core::char::methods::EscapeDebugExtArgs"
                [
                  ("escape_grapheme_extended", Value.Bool true);
                  ("escape_single_quote", Value.Bool true);
                  ("escape_double_quote", Value.Bool true)
                ]
            |))).
      
      Axiom AssociatedConstant_value_ESCAPE_ALL :
        M.IsAssociatedConstant Self "value_ESCAPE_ALL" value_ESCAPE_ALL.
    End Impl_core_char_methods_EscapeDebugExtArgs.
    
    (*
    const fn len_utf8(code: u32) -> usize {
        match code {
            ..MAX_ONE_B => 1,
            ..MAX_TWO_B => 2,
            ..MAX_THREE_B => 3,
            _ => 4,
        }
    }
    *)
    Definition len_utf8 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ code ] =>
        ltac:(M.monadic
          (let code := M.alloc (| code |) in
          M.read (|
            M.match_operator (|
              code,
              [
                fun γ => ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 1 |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 2 |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 3 |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 4 |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_len_utf8 : M.IsFunction "core::char::methods::len_utf8" len_utf8.
    
    (*
    const fn len_utf16(code: u32) -> usize {
        if (code & 0xFFFF) == code { 1 } else { 2 }
    }
    *)
    Definition len_utf16 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ code ] =>
        ltac:(M.monadic
          (let code := M.alloc (| code |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          BinOp.eq (|
                            BinOp.bit_and (M.read (| code |)) (Value.Integer IntegerKind.U32 65535),
                            M.read (| code |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (| Value.Integer IntegerKind.Usize 1 |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 2 |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_len_utf16 : M.IsFunction "core::char::methods::len_utf16" len_utf16.
    
    (*
    pub const fn encode_utf8_raw(code: u32, dst: &mut [u8]) -> &mut [u8] {
        const fn panic_at_const(_code: u32, _len: usize, _dst_len: usize) {
            // Note that we cannot format in constant expressions.
            panic!("encode_utf8: buffer does not have enough bytes to encode code point");
        }
        fn panic_at_rt(code: u32, len: usize, dst_len: usize) {
            panic!(
                "encode_utf8: need {len} bytes to encode U+{code:04X} but buffer has just {dst_len}",
            );
        }
        let len = len_utf8(code);
        match (len, &mut *dst) {
            (1, [a, ..]) => {
                *a = code as u8;
            }
            (2, [a, b, ..]) => {
                *a = (code >> 6 & 0x1F) as u8 | TAG_TWO_B;
                *b = (code & 0x3F) as u8 | TAG_CONT;
            }
            (3, [a, b, c, ..]) => {
                *a = (code >> 12 & 0x0F) as u8 | TAG_THREE_B;
                *b = (code >> 6 & 0x3F) as u8 | TAG_CONT;
                *c = (code & 0x3F) as u8 | TAG_CONT;
            }
            (4, [a, b, c, d, ..]) => {
                *a = (code >> 18 & 0x07) as u8 | TAG_FOUR_B;
                *b = (code >> 12 & 0x3F) as u8 | TAG_CONT;
                *c = (code >> 6 & 0x3F) as u8 | TAG_CONT;
                *d = (code & 0x3F) as u8 | TAG_CONT;
            }
            // FIXME(const-hack): We would prefer to have streamlined panics when formatters become const-friendly.
            _ => const_eval_select((code, len, dst.len()), panic_at_const, panic_at_rt),
        };
        // SAFETY: `<&mut [u8]>::as_mut_ptr` is guaranteed to return a valid pointer and `len` has been tested to be within bounds.
        unsafe { slice::from_raw_parts_mut(dst.as_mut_ptr(), len) }
    }
    *)
    Definition encode_utf8_raw (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ code; dst ] =>
        ltac:(M.monadic
          (let code := M.alloc (| code |) in
          let dst := M.alloc (| dst |) in
          M.read (|
            let~ len :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::char::methods::len_utf8", [] |),
                  [ M.read (| code |) ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [ M.read (| len |); M.read (| dst |) ] |),
                [
                  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_constant_or_break_match (|
                          M.read (| γ0_0 |),
                          Value.Integer IntegerKind.Usize 1
                        |) in
                      let γ0_1 := M.read (| γ0_1 |) in
                      let γ2_0 := M.SubPointer.get_slice_index (| γ0_1, 0 |) in
                      let γ2_rest := M.SubPointer.get_slice_rest (| γ0_1, 1, 0 |) in
                      let a := M.alloc (| γ2_0 |) in
                      let~ _ := M.write (| M.read (| a |), M.rust_cast (M.read (| code |)) |) in
                      M.alloc (| Value.Tuple [] |)));
                  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_constant_or_break_match (|
                          M.read (| γ0_0 |),
                          Value.Integer IntegerKind.Usize 2
                        |) in
                      let γ0_1 := M.read (| γ0_1 |) in
                      let γ2_0 := M.SubPointer.get_slice_index (| γ0_1, 0 |) in
                      let γ2_1 := M.SubPointer.get_slice_index (| γ0_1, 1 |) in
                      let γ2_rest := M.SubPointer.get_slice_rest (| γ0_1, 2, 0 |) in
                      let a := M.alloc (| γ2_0 |) in
                      let b := M.alloc (| γ2_1 |) in
                      let~ _ :=
                        M.write (|
                          M.read (| a |),
                          BinOp.bit_or
                            (M.rust_cast
                              (BinOp.bit_and
                                (BinOp.Wrap.shr (|
                                  M.read (| code |),
                                  Value.Integer IntegerKind.I32 6
                                |))
                                (Value.Integer IntegerKind.U32 31)))
                            (M.read (| M.get_constant (| "core::char::TAG_TWO_B" |) |))
                        |) in
                      let~ _ :=
                        M.write (|
                          M.read (| b |),
                          BinOp.bit_or
                            (M.rust_cast
                              (BinOp.bit_and
                                (M.read (| code |))
                                (Value.Integer IntegerKind.U32 63)))
                            (M.read (| M.get_constant (| "core::char::TAG_CONT" |) |))
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  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_constant_or_break_match (|
                          M.read (| γ0_0 |),
                          Value.Integer IntegerKind.Usize 3
                        |) in
                      let γ0_1 := M.read (| γ0_1 |) in
                      let γ2_0 := M.SubPointer.get_slice_index (| γ0_1, 0 |) in
                      let γ2_1 := M.SubPointer.get_slice_index (| γ0_1, 1 |) in
                      let γ2_2 := M.SubPointer.get_slice_index (| γ0_1, 2 |) in
                      let γ2_rest := M.SubPointer.get_slice_rest (| γ0_1, 3, 0 |) in
                      let a := M.alloc (| γ2_0 |) in
                      let b := M.alloc (| γ2_1 |) in
                      let c := M.alloc (| γ2_2 |) in
                      let~ _ :=
                        M.write (|
                          M.read (| a |),
                          BinOp.bit_or
                            (M.rust_cast
                              (BinOp.bit_and
                                (BinOp.Wrap.shr (|
                                  M.read (| code |),
                                  Value.Integer IntegerKind.I32 12
                                |))
                                (Value.Integer IntegerKind.U32 15)))
                            (M.read (| M.get_constant (| "core::char::TAG_THREE_B" |) |))
                        |) in
                      let~ _ :=
                        M.write (|
                          M.read (| b |),
                          BinOp.bit_or
                            (M.rust_cast
                              (BinOp.bit_and
                                (BinOp.Wrap.shr (|
                                  M.read (| code |),
                                  Value.Integer IntegerKind.I32 6
                                |))
                                (Value.Integer IntegerKind.U32 63)))
                            (M.read (| M.get_constant (| "core::char::TAG_CONT" |) |))
                        |) in
                      let~ _ :=
                        M.write (|
                          M.read (| c |),
                          BinOp.bit_or
                            (M.rust_cast
                              (BinOp.bit_and
                                (M.read (| code |))
                                (Value.Integer IntegerKind.U32 63)))
                            (M.read (| M.get_constant (| "core::char::TAG_CONT" |) |))
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  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_constant_or_break_match (|
                          M.read (| γ0_0 |),
                          Value.Integer IntegerKind.Usize 4
                        |) in
                      let γ0_1 := M.read (| γ0_1 |) in
                      let γ2_0 := M.SubPointer.get_slice_index (| γ0_1, 0 |) in
                      let γ2_1 := M.SubPointer.get_slice_index (| γ0_1, 1 |) in
                      let γ2_2 := M.SubPointer.get_slice_index (| γ0_1, 2 |) in
                      let γ2_3 := M.SubPointer.get_slice_index (| γ0_1, 3 |) in
                      let γ2_rest := M.SubPointer.get_slice_rest (| γ0_1, 4, 0 |) in
                      let a := M.alloc (| γ2_0 |) in
                      let b := M.alloc (| γ2_1 |) in
                      let c := M.alloc (| γ2_2 |) in
                      let d := M.alloc (| γ2_3 |) in
                      let~ _ :=
                        M.write (|
                          M.read (| a |),
                          BinOp.bit_or
                            (M.rust_cast
                              (BinOp.bit_and
                                (BinOp.Wrap.shr (|
                                  M.read (| code |),
                                  Value.Integer IntegerKind.I32 18
                                |))
                                (Value.Integer IntegerKind.U32 7)))
                            (M.read (| M.get_constant (| "core::char::TAG_FOUR_B" |) |))
                        |) in
                      let~ _ :=
                        M.write (|
                          M.read (| b |),
                          BinOp.bit_or
                            (M.rust_cast
                              (BinOp.bit_and
                                (BinOp.Wrap.shr (|
                                  M.read (| code |),
                                  Value.Integer IntegerKind.I32 12
                                |))
                                (Value.Integer IntegerKind.U32 63)))
                            (M.read (| M.get_constant (| "core::char::TAG_CONT" |) |))
                        |) in
                      let~ _ :=
                        M.write (|
                          M.read (| c |),
                          BinOp.bit_or
                            (M.rust_cast
                              (BinOp.bit_and
                                (BinOp.Wrap.shr (|
                                  M.read (| code |),
                                  Value.Integer IntegerKind.I32 6
                                |))
                                (Value.Integer IntegerKind.U32 63)))
                            (M.read (| M.get_constant (| "core::char::TAG_CONT" |) |))
                        |) in
                      let~ _ :=
                        M.write (|
                          M.read (| d |),
                          BinOp.bit_or
                            (M.rust_cast
                              (BinOp.bit_and
                                (M.read (| code |))
                                (Value.Integer IntegerKind.U32 63)))
                            (M.read (| M.get_constant (| "core::char::TAG_CONT" |) |))
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::intrinsics::const_eval_select",
                            [
                              Ty.tuple [ Ty.path "u32"; Ty.path "usize"; Ty.path "usize" ];
                              Ty.function
                                [ Ty.path "u32"; Ty.path "usize"; Ty.path "usize" ]
                                (Ty.tuple []);
                              Ty.function
                                [ Ty.path "u32"; Ty.path "usize"; Ty.path "usize" ]
                                (Ty.tuple []);
                              Ty.tuple []
                            ]
                          |),
                          [
                            Value.Tuple
                              [
                                M.read (| code |);
                                M.read (| len |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| dst |) ]
                                |)
                              ];
                            M.get_function (|
                              "core::char::methods::encode_utf8_raw.panic_at_const",
                              []
                            |);
                            M.get_function (|
                              "core::char::methods::encode_utf8_raw.panic_at_rt",
                              []
                            |)
                          ]
                        |)
                      |)))
                ]
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::slice::raw::from_raw_parts_mut", [ Ty.path "u8" ] |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                      "as_mut_ptr",
                      []
                    |),
                    [ M.read (| dst |) ]
                  |);
                  M.read (| len |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_encode_utf8_raw :
      M.IsFunction "core::char::methods::encode_utf8_raw" encode_utf8_raw.
    
    Module encode_utf8_raw.
      (*
          const fn panic_at_const(_code: u32, _len: usize, _dst_len: usize) {
              // Note that we cannot format in constant expressions.
              panic!("encode_utf8: buffer does not have enough bytes to encode code point");
          }
      *)
      Definition panic_at_const (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ _code; _len; _dst_len ] =>
          ltac:(M.monadic
            (let _code := M.alloc (| _code |) in
            let _len := M.alloc (| _len |) in
            let _dst_len := M.alloc (| _dst_len |) in
            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
                                "encode_utf8: buffer does not have enough bytes to encode code point"
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_panic_at_const :
        M.IsFunction "core::char::methods::encode_utf8_raw::panic_at_const" panic_at_const.
      
      (*
          fn panic_at_rt(code: u32, len: usize, dst_len: usize) {
              panic!(
                  "encode_utf8: need {len} bytes to encode U+{code:04X} but buffer has just {dst_len}",
              );
          }
      *)
      Definition panic_at_rt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ code; len; dst_len ] =>
          ltac:(M.monadic
            (let code := M.alloc (| code |) in
            let len := M.alloc (| len |) in
            let dst_len := M.alloc (| dst_len |) in
            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_v1_formatted",
                      []
                    |),
                    [
                      M.alloc (|
                        Value.Array
                          [
                            M.read (| Value.String "encode_utf8: need " |);
                            M.read (| Value.String " bytes to encode U+" |);
                            M.read (| Value.String " but buffer has just " |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_display",
                                [ Ty.path "usize" ]
                              |),
                              [ len ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_upper_hex",
                                [ Ty.path "u32" ]
                              |),
                              [ code ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_display",
                                [ Ty.path "usize" ]
                              |),
                              [ dst_len ]
                            |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Placeholder",
                                "new",
                                []
                              |),
                              [
                                Value.Integer IntegerKind.Usize 0;
                                Value.UnicodeChar 32;
                                Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                Value.Integer IntegerKind.U32 0;
                                Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                Value.StructTuple "core::fmt::rt::Count::Implied" []
                              ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Placeholder",
                                "new",
                                []
                              |),
                              [
                                Value.Integer IntegerKind.Usize 1;
                                Value.UnicodeChar 32;
                                Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                Value.Integer IntegerKind.U32 8;
                                Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                Value.StructTuple
                                  "core::fmt::rt::Count::Is"
                                  [ Value.Integer IntegerKind.Usize 4 ]
                              ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Placeholder",
                                "new",
                                []
                              |),
                              [
                                Value.Integer IntegerKind.Usize 2;
                                Value.UnicodeChar 32;
                                Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                Value.Integer IntegerKind.U32 0;
                                Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                Value.StructTuple "core::fmt::rt::Count::Implied" []
                              ]
                            |)
                          ]
                      |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::rt::UnsafeArg",
                          "new",
                          []
                        |),
                        []
                      |)
                    ]
                  |)
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_panic_at_rt :
        M.IsFunction "core::char::methods::encode_utf8_raw::panic_at_rt" panic_at_rt.
    End encode_utf8_raw.
    
    (*
    pub const fn encode_utf16_raw(mut code: u32, dst: &mut [u16]) -> &mut [u16] {
        const fn panic_at_const(_code: u32, _len: usize, _dst_len: usize) {
            // Note that we cannot format in constant expressions.
            panic!("encode_utf16: buffer does not have enough bytes to encode code point");
        }
        fn panic_at_rt(code: u32, len: usize, dst_len: usize) {
            panic!(
                "encode_utf16: need {len} bytes to encode U+{code:04X} but buffer has just {dst_len}",
            );
        }
        let len = len_utf16(code);
        match (len, &mut *dst) {
            (1, [a, ..]) => {
                *a = code as u16;
            }
            (2, [a, b, ..]) => {
                code -= 0x1_0000;
    
                *a = (code >> 10) as u16 | 0xD800;
                *b = (code & 0x3FF) as u16 | 0xDC00;
            }
            // FIXME(const-hack): We would prefer to have streamlined panics when formatters become const-friendly.
            _ => const_eval_select((code, len, dst.len()), panic_at_const, panic_at_rt),
        };
        // SAFETY: `<&mut [u16]>::as_mut_ptr` is guaranteed to return a valid pointer and `len` has been tested to be within bounds.
        unsafe { slice::from_raw_parts_mut(dst.as_mut_ptr(), len) }
    }
    *)
    Definition encode_utf16_raw (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ code; dst ] =>
        ltac:(M.monadic
          (let code := M.alloc (| code |) in
          let dst := M.alloc (| dst |) in
          M.read (|
            let~ len :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::char::methods::len_utf16", [] |),
                  [ M.read (| code |) ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [ M.read (| len |); M.read (| dst |) ] |),
                [
                  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_constant_or_break_match (|
                          M.read (| γ0_0 |),
                          Value.Integer IntegerKind.Usize 1
                        |) in
                      let γ0_1 := M.read (| γ0_1 |) in
                      let γ2_0 := M.SubPointer.get_slice_index (| γ0_1, 0 |) in
                      let γ2_rest := M.SubPointer.get_slice_rest (| γ0_1, 1, 0 |) in
                      let a := M.alloc (| γ2_0 |) in
                      let~ _ := M.write (| M.read (| a |), M.rust_cast (M.read (| code |)) |) in
                      M.alloc (| Value.Tuple [] |)));
                  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_constant_or_break_match (|
                          M.read (| γ0_0 |),
                          Value.Integer IntegerKind.Usize 2
                        |) in
                      let γ0_1 := M.read (| γ0_1 |) in
                      let γ2_0 := M.SubPointer.get_slice_index (| γ0_1, 0 |) in
                      let γ2_1 := M.SubPointer.get_slice_index (| γ0_1, 1 |) in
                      let γ2_rest := M.SubPointer.get_slice_rest (| γ0_1, 2, 0 |) in
                      let a := M.alloc (| γ2_0 |) in
                      let b := M.alloc (| γ2_1 |) in
                      let~ _ :=
                        let β := code in
                        M.write (|
                          β,
                          BinOp.Wrap.sub (| M.read (| β |), Value.Integer IntegerKind.U32 65536 |)
                        |) in
                      let~ _ :=
                        M.write (|
                          M.read (| a |),
                          BinOp.bit_or
                            (M.rust_cast
                              (BinOp.Wrap.shr (|
                                M.read (| code |),
                                Value.Integer IntegerKind.I32 10
                              |)))
                            (Value.Integer IntegerKind.U16 55296)
                        |) in
                      let~ _ :=
                        M.write (|
                          M.read (| b |),
                          BinOp.bit_or
                            (M.rust_cast
                              (BinOp.bit_and
                                (M.read (| code |))
                                (Value.Integer IntegerKind.U32 1023)))
                            (Value.Integer IntegerKind.U16 56320)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::intrinsics::const_eval_select",
                            [
                              Ty.tuple [ Ty.path "u32"; Ty.path "usize"; Ty.path "usize" ];
                              Ty.function
                                [ Ty.path "u32"; Ty.path "usize"; Ty.path "usize" ]
                                (Ty.tuple []);
                              Ty.function
                                [ Ty.path "u32"; Ty.path "usize"; Ty.path "usize" ]
                                (Ty.tuple []);
                              Ty.tuple []
                            ]
                          |),
                          [
                            Value.Tuple
                              [
                                M.read (| code |);
                                M.read (| len |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u16" ],
                                    "len",
                                    []
                                  |),
                                  [ M.read (| dst |) ]
                                |)
                              ];
                            M.get_function (|
                              "core::char::methods::encode_utf16_raw.panic_at_const",
                              []
                            |);
                            M.get_function (|
                              "core::char::methods::encode_utf16_raw.panic_at_rt",
                              []
                            |)
                          ]
                        |)
                      |)))
                ]
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_function (| "core::slice::raw::from_raw_parts_mut", [ Ty.path "u16" ] |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "slice") [] [ Ty.path "u16" ],
                      "as_mut_ptr",
                      []
                    |),
                    [ M.read (| dst |) ]
                  |);
                  M.read (| len |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_encode_utf16_raw :
      M.IsFunction "core::char::methods::encode_utf16_raw" encode_utf16_raw.
    
    Module encode_utf16_raw.
      (*
          const fn panic_at_const(_code: u32, _len: usize, _dst_len: usize) {
              // Note that we cannot format in constant expressions.
              panic!("encode_utf16: buffer does not have enough bytes to encode code point");
          }
      *)
      Definition panic_at_const (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ _code; _len; _dst_len ] =>
          ltac:(M.monadic
            (let _code := M.alloc (| _code |) in
            let _len := M.alloc (| _len |) in
            let _dst_len := M.alloc (| _dst_len |) in
            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
                                "encode_utf16: buffer does not have enough bytes to encode code point"
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_panic_at_const :
        M.IsFunction "core::char::methods::encode_utf16_raw::panic_at_const" panic_at_const.
      
      (*
          fn panic_at_rt(code: u32, len: usize, dst_len: usize) {
              panic!(
                  "encode_utf16: need {len} bytes to encode U+{code:04X} but buffer has just {dst_len}",
              );
          }
      *)
      Definition panic_at_rt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ code; len; dst_len ] =>
          ltac:(M.monadic
            (let code := M.alloc (| code |) in
            let len := M.alloc (| len |) in
            let dst_len := M.alloc (| dst_len |) in
            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_v1_formatted",
                      []
                    |),
                    [
                      M.alloc (|
                        Value.Array
                          [
                            M.read (| Value.String "encode_utf16: need " |);
                            M.read (| Value.String " bytes to encode U+" |);
                            M.read (| Value.String " but buffer has just " |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_display",
                                [ Ty.path "usize" ]
                              |),
                              [ len ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_upper_hex",
                                [ Ty.path "u32" ]
                              |),
                              [ code ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_display",
                                [ Ty.path "usize" ]
                              |),
                              [ dst_len ]
                            |)
                          ]
                      |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Placeholder",
                                "new",
                                []
                              |),
                              [
                                Value.Integer IntegerKind.Usize 0;
                                Value.UnicodeChar 32;
                                Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                Value.Integer IntegerKind.U32 0;
                                Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                Value.StructTuple "core::fmt::rt::Count::Implied" []
                              ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Placeholder",
                                "new",
                                []
                              |),
                              [
                                Value.Integer IntegerKind.Usize 1;
                                Value.UnicodeChar 32;
                                Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                Value.Integer IntegerKind.U32 8;
                                Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                Value.StructTuple
                                  "core::fmt::rt::Count::Is"
                                  [ Value.Integer IntegerKind.Usize 4 ]
                              ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Placeholder",
                                "new",
                                []
                              |),
                              [
                                Value.Integer IntegerKind.Usize 2;
                                Value.UnicodeChar 32;
                                Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                Value.Integer IntegerKind.U32 0;
                                Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                Value.StructTuple "core::fmt::rt::Count::Implied" []
                              ]
                            |)
                          ]
                      |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::rt::UnsafeArg",
                          "new",
                          []
                        |),
                        []
                      |)
                    ]
                  |)
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Function_panic_at_rt :
        M.IsFunction "core::char::methods::encode_utf16_raw::panic_at_rt" panic_at_rt.
    End encode_utf16_raw.
  End methods.
End char.
