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

Module ascii.
  Module ascii_char.
    (*
    Enum AsciiChar
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "Null";
            item := StructTuple [];
            discriminant := Some 0;
          };
          {
            name := "StartOfHeading";
            item := StructTuple [];
            discriminant := Some 1;
          };
          {
            name := "StartOfText";
            item := StructTuple [];
            discriminant := Some 2;
          };
          {
            name := "EndOfText";
            item := StructTuple [];
            discriminant := Some 3;
          };
          {
            name := "EndOfTransmission";
            item := StructTuple [];
            discriminant := Some 4;
          };
          {
            name := "Enquiry";
            item := StructTuple [];
            discriminant := Some 5;
          };
          {
            name := "Acknowledge";
            item := StructTuple [];
            discriminant := Some 6;
          };
          {
            name := "Bell";
            item := StructTuple [];
            discriminant := Some 7;
          };
          {
            name := "Backspace";
            item := StructTuple [];
            discriminant := Some 8;
          };
          {
            name := "CharacterTabulation";
            item := StructTuple [];
            discriminant := Some 9;
          };
          {
            name := "LineFeed";
            item := StructTuple [];
            discriminant := Some 10;
          };
          {
            name := "LineTabulation";
            item := StructTuple [];
            discriminant := Some 11;
          };
          {
            name := "FormFeed";
            item := StructTuple [];
            discriminant := Some 12;
          };
          {
            name := "CarriageReturn";
            item := StructTuple [];
            discriminant := Some 13;
          };
          {
            name := "ShiftOut";
            item := StructTuple [];
            discriminant := Some 14;
          };
          {
            name := "ShiftIn";
            item := StructTuple [];
            discriminant := Some 15;
          };
          {
            name := "DataLinkEscape";
            item := StructTuple [];
            discriminant := Some 16;
          };
          {
            name := "DeviceControlOne";
            item := StructTuple [];
            discriminant := Some 17;
          };
          {
            name := "DeviceControlTwo";
            item := StructTuple [];
            discriminant := Some 18;
          };
          {
            name := "DeviceControlThree";
            item := StructTuple [];
            discriminant := Some 19;
          };
          {
            name := "DeviceControlFour";
            item := StructTuple [];
            discriminant := Some 20;
          };
          {
            name := "NegativeAcknowledge";
            item := StructTuple [];
            discriminant := Some 21;
          };
          {
            name := "SynchronousIdle";
            item := StructTuple [];
            discriminant := Some 22;
          };
          {
            name := "EndOfTransmissionBlock";
            item := StructTuple [];
            discriminant := Some 23;
          };
          {
            name := "Cancel";
            item := StructTuple [];
            discriminant := Some 24;
          };
          {
            name := "EndOfMedium";
            item := StructTuple [];
            discriminant := Some 25;
          };
          {
            name := "Substitute";
            item := StructTuple [];
            discriminant := Some 26;
          };
          {
            name := "Escape";
            item := StructTuple [];
            discriminant := Some 27;
          };
          {
            name := "InformationSeparatorFour";
            item := StructTuple [];
            discriminant := Some 28;
          };
          {
            name := "InformationSeparatorThree";
            item := StructTuple [];
            discriminant := Some 29;
          };
          {
            name := "InformationSeparatorTwo";
            item := StructTuple [];
            discriminant := Some 30;
          };
          {
            name := "InformationSeparatorOne";
            item := StructTuple [];
            discriminant := Some 31;
          };
          {
            name := "Space";
            item := StructTuple [];
            discriminant := Some 32;
          };
          {
            name := "ExclamationMark";
            item := StructTuple [];
            discriminant := Some 33;
          };
          {
            name := "QuotationMark";
            item := StructTuple [];
            discriminant := Some 34;
          };
          {
            name := "NumberSign";
            item := StructTuple [];
            discriminant := Some 35;
          };
          {
            name := "DollarSign";
            item := StructTuple [];
            discriminant := Some 36;
          };
          {
            name := "PercentSign";
            item := StructTuple [];
            discriminant := Some 37;
          };
          {
            name := "Ampersand";
            item := StructTuple [];
            discriminant := Some 38;
          };
          {
            name := "Apostrophe";
            item := StructTuple [];
            discriminant := Some 39;
          };
          {
            name := "LeftParenthesis";
            item := StructTuple [];
            discriminant := Some 40;
          };
          {
            name := "RightParenthesis";
            item := StructTuple [];
            discriminant := Some 41;
          };
          {
            name := "Asterisk";
            item := StructTuple [];
            discriminant := Some 42;
          };
          {
            name := "PlusSign";
            item := StructTuple [];
            discriminant := Some 43;
          };
          {
            name := "Comma";
            item := StructTuple [];
            discriminant := Some 44;
          };
          {
            name := "HyphenMinus";
            item := StructTuple [];
            discriminant := Some 45;
          };
          {
            name := "FullStop";
            item := StructTuple [];
            discriminant := Some 46;
          };
          {
            name := "Solidus";
            item := StructTuple [];
            discriminant := Some 47;
          };
          {
            name := "Digit0";
            item := StructTuple [];
            discriminant := Some 48;
          };
          {
            name := "Digit1";
            item := StructTuple [];
            discriminant := Some 49;
          };
          {
            name := "Digit2";
            item := StructTuple [];
            discriminant := Some 50;
          };
          {
            name := "Digit3";
            item := StructTuple [];
            discriminant := Some 51;
          };
          {
            name := "Digit4";
            item := StructTuple [];
            discriminant := Some 52;
          };
          {
            name := "Digit5";
            item := StructTuple [];
            discriminant := Some 53;
          };
          {
            name := "Digit6";
            item := StructTuple [];
            discriminant := Some 54;
          };
          {
            name := "Digit7";
            item := StructTuple [];
            discriminant := Some 55;
          };
          {
            name := "Digit8";
            item := StructTuple [];
            discriminant := Some 56;
          };
          {
            name := "Digit9";
            item := StructTuple [];
            discriminant := Some 57;
          };
          {
            name := "Colon";
            item := StructTuple [];
            discriminant := Some 58;
          };
          {
            name := "Semicolon";
            item := StructTuple [];
            discriminant := Some 59;
          };
          {
            name := "LessThanSign";
            item := StructTuple [];
            discriminant := Some 60;
          };
          {
            name := "EqualsSign";
            item := StructTuple [];
            discriminant := Some 61;
          };
          {
            name := "GreaterThanSign";
            item := StructTuple [];
            discriminant := Some 62;
          };
          {
            name := "QuestionMark";
            item := StructTuple [];
            discriminant := Some 63;
          };
          {
            name := "CommercialAt";
            item := StructTuple [];
            discriminant := Some 64;
          };
          {
            name := "CapitalA";
            item := StructTuple [];
            discriminant := Some 65;
          };
          {
            name := "CapitalB";
            item := StructTuple [];
            discriminant := Some 66;
          };
          {
            name := "CapitalC";
            item := StructTuple [];
            discriminant := Some 67;
          };
          {
            name := "CapitalD";
            item := StructTuple [];
            discriminant := Some 68;
          };
          {
            name := "CapitalE";
            item := StructTuple [];
            discriminant := Some 69;
          };
          {
            name := "CapitalF";
            item := StructTuple [];
            discriminant := Some 70;
          };
          {
            name := "CapitalG";
            item := StructTuple [];
            discriminant := Some 71;
          };
          {
            name := "CapitalH";
            item := StructTuple [];
            discriminant := Some 72;
          };
          {
            name := "CapitalI";
            item := StructTuple [];
            discriminant := Some 73;
          };
          {
            name := "CapitalJ";
            item := StructTuple [];
            discriminant := Some 74;
          };
          {
            name := "CapitalK";
            item := StructTuple [];
            discriminant := Some 75;
          };
          {
            name := "CapitalL";
            item := StructTuple [];
            discriminant := Some 76;
          };
          {
            name := "CapitalM";
            item := StructTuple [];
            discriminant := Some 77;
          };
          {
            name := "CapitalN";
            item := StructTuple [];
            discriminant := Some 78;
          };
          {
            name := "CapitalO";
            item := StructTuple [];
            discriminant := Some 79;
          };
          {
            name := "CapitalP";
            item := StructTuple [];
            discriminant := Some 80;
          };
          {
            name := "CapitalQ";
            item := StructTuple [];
            discriminant := Some 81;
          };
          {
            name := "CapitalR";
            item := StructTuple [];
            discriminant := Some 82;
          };
          {
            name := "CapitalS";
            item := StructTuple [];
            discriminant := Some 83;
          };
          {
            name := "CapitalT";
            item := StructTuple [];
            discriminant := Some 84;
          };
          {
            name := "CapitalU";
            item := StructTuple [];
            discriminant := Some 85;
          };
          {
            name := "CapitalV";
            item := StructTuple [];
            discriminant := Some 86;
          };
          {
            name := "CapitalW";
            item := StructTuple [];
            discriminant := Some 87;
          };
          {
            name := "CapitalX";
            item := StructTuple [];
            discriminant := Some 88;
          };
          {
            name := "CapitalY";
            item := StructTuple [];
            discriminant := Some 89;
          };
          {
            name := "CapitalZ";
            item := StructTuple [];
            discriminant := Some 90;
          };
          {
            name := "LeftSquareBracket";
            item := StructTuple [];
            discriminant := Some 91;
          };
          {
            name := "ReverseSolidus";
            item := StructTuple [];
            discriminant := Some 92;
          };
          {
            name := "RightSquareBracket";
            item := StructTuple [];
            discriminant := Some 93;
          };
          {
            name := "CircumflexAccent";
            item := StructTuple [];
            discriminant := Some 94;
          };
          {
            name := "LowLine";
            item := StructTuple [];
            discriminant := Some 95;
          };
          {
            name := "GraveAccent";
            item := StructTuple [];
            discriminant := Some 96;
          };
          {
            name := "SmallA";
            item := StructTuple [];
            discriminant := Some 97;
          };
          {
            name := "SmallB";
            item := StructTuple [];
            discriminant := Some 98;
          };
          {
            name := "SmallC";
            item := StructTuple [];
            discriminant := Some 99;
          };
          {
            name := "SmallD";
            item := StructTuple [];
            discriminant := Some 100;
          };
          {
            name := "SmallE";
            item := StructTuple [];
            discriminant := Some 101;
          };
          {
            name := "SmallF";
            item := StructTuple [];
            discriminant := Some 102;
          };
          {
            name := "SmallG";
            item := StructTuple [];
            discriminant := Some 103;
          };
          {
            name := "SmallH";
            item := StructTuple [];
            discriminant := Some 104;
          };
          {
            name := "SmallI";
            item := StructTuple [];
            discriminant := Some 105;
          };
          {
            name := "SmallJ";
            item := StructTuple [];
            discriminant := Some 106;
          };
          {
            name := "SmallK";
            item := StructTuple [];
            discriminant := Some 107;
          };
          {
            name := "SmallL";
            item := StructTuple [];
            discriminant := Some 108;
          };
          {
            name := "SmallM";
            item := StructTuple [];
            discriminant := Some 109;
          };
          {
            name := "SmallN";
            item := StructTuple [];
            discriminant := Some 110;
          };
          {
            name := "SmallO";
            item := StructTuple [];
            discriminant := Some 111;
          };
          {
            name := "SmallP";
            item := StructTuple [];
            discriminant := Some 112;
          };
          {
            name := "SmallQ";
            item := StructTuple [];
            discriminant := Some 113;
          };
          {
            name := "SmallR";
            item := StructTuple [];
            discriminant := Some 114;
          };
          {
            name := "SmallS";
            item := StructTuple [];
            discriminant := Some 115;
          };
          {
            name := "SmallT";
            item := StructTuple [];
            discriminant := Some 116;
          };
          {
            name := "SmallU";
            item := StructTuple [];
            discriminant := Some 117;
          };
          {
            name := "SmallV";
            item := StructTuple [];
            discriminant := Some 118;
          };
          {
            name := "SmallW";
            item := StructTuple [];
            discriminant := Some 119;
          };
          {
            name := "SmallX";
            item := StructTuple [];
            discriminant := Some 120;
          };
          {
            name := "SmallY";
            item := StructTuple [];
            discriminant := Some 121;
          };
          {
            name := "SmallZ";
            item := StructTuple [];
            discriminant := Some 122;
          };
          {
            name := "LeftCurlyBracket";
            item := StructTuple [];
            discriminant := Some 123;
          };
          {
            name := "VerticalLine";
            item := StructTuple [];
            discriminant := Some 124;
          };
          {
            name := "RightCurlyBracket";
            item := StructTuple [];
            discriminant := Some 125;
          };
          {
            name := "Tilde";
            item := StructTuple [];
            discriminant := Some 126;
          };
          {
            name := "Delete";
            item := StructTuple [];
            discriminant := Some 127;
          }
        ];
    }
    *)
    
    Module Impl_core_marker_Copy_for_core_ascii_ascii_char_AsciiChar.
      Definition Self : Ty.t := Ty.path "core::ascii::ascii_char::AsciiChar".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_core_ascii_ascii_char_AsciiChar.
    
    Module Impl_core_clone_Clone_for_core_ascii_ascii_char_AsciiChar.
      Definition Self : Ty.t := Ty.path "core::ascii::ascii_char::AsciiChar".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_core_ascii_ascii_char_AsciiChar.
    
    Module Impl_core_cmp_Eq_for_core_ascii_ascii_char_AsciiChar.
      Definition Self : Ty.t := Ty.path "core::ascii::ascii_char::AsciiChar".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.Tuple []))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_core_ascii_ascii_char_AsciiChar.
    
    Module Impl_core_marker_StructuralPartialEq_for_core_ascii_ascii_char_AsciiChar.
      Definition Self : Ty.t := Ty.path "core::ascii::ascii_char::AsciiChar".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_core_ascii_ascii_char_AsciiChar.
    
    Module Impl_core_cmp_PartialEq_for_core_ascii_ascii_char_AsciiChar.
      Definition Self : Ty.t := Ty.path "core::ascii::ascii_char::AsciiChar".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::ascii::ascii_char::AsciiChar" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::ascii::ascii_char::AsciiChar" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_core_ascii_ascii_char_AsciiChar.
    
    Module Impl_core_cmp_Ord_for_core_ascii_ascii_char_AsciiChar.
      Definition Self : Ty.t := Ty.path "core::ascii::ascii_char::AsciiChar".
      
      (* Ord *)
      Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::ascii::ascii_char::AsciiChar" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::ascii::ascii_char::AsciiChar" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::cmp::Ord", Ty.path "u8", [], "cmp", [] |),
                  [ __self_discr; __arg1_discr ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Ord"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
    End Impl_core_cmp_Ord_for_core_ascii_ascii_char_AsciiChar.
    
    Module Impl_core_cmp_PartialOrd_for_core_ascii_ascii_char_AsciiChar.
      Definition Self : Ty.t := Ty.path "core::ascii::ascii_char::AsciiChar".
      
      (* PartialOrd *)
      Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::ascii::ascii_char::AsciiChar" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::ascii::ascii_char::AsciiChar" ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialOrd",
                    Ty.path "u8",
                    [ Ty.path "u8" ],
                    "partial_cmp",
                    []
                  |),
                  [ __self_discr; __arg1_discr ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialOrd"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
    End Impl_core_cmp_PartialOrd_for_core_ascii_ascii_char_AsciiChar.
    
    Module Impl_core_hash_Hash_for_core_ascii_ascii_char_AsciiChar.
      Definition Self : Ty.t := Ty.path "core::ascii::ascii_char::AsciiChar".
      
      (* Hash *)
      Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ __H ], [ self; state ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let state := M.alloc (| state |) in
            M.read (|
              let~ __self_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "core::ascii::ascii_char::AsciiChar" ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Ty.path "u8", [], "hash", [ __H ] |),
                  [ __self_discr; M.read (| state |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::hash::Hash"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("hash", InstanceField.Method hash) ].
    End Impl_core_hash_Hash_for_core_ascii_ascii_char_AsciiChar.
    
    Module Impl_core_ascii_ascii_char_AsciiChar.
      Definition Self : Ty.t := Ty.path "core::ascii::ascii_char::AsciiChar".
      
      (*
          pub const fn from_u8(b: u8) -> Option<Self> {
              if b <= 127 {
                  // SAFETY: Just checked that `b` is in-range
                  Some(unsafe { Self::from_u8_unchecked(b) })
              } else {
                  None
              }
          }
      *)
      Definition from_u8 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ b ] =>
          ltac:(M.monadic
            (let b := M.alloc (| b |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.le (| M.read (| b |), Value.Integer IntegerKind.U8 127 |)
                          |)) 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.read (| b |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_u8 : M.IsAssociatedFunction Self "from_u8" from_u8.
      
      (*
          pub const unsafe fn from_u8_unchecked(b: u8) -> Self {
              // SAFETY: Our safety precondition is that `b` is in-range.
              unsafe { transmute(b) }
          }
      *)
      Definition from_u8_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ b ] =>
          ltac:(M.monadic
            (let b := M.alloc (| b |) in
            M.call_closure (|
              M.get_function (|
                "core::intrinsics::transmute",
                [ Ty.path "u8"; Ty.path "core::ascii::ascii_char::AsciiChar" ]
              |),
              [ M.read (| b |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_from_u8_unchecked :
        M.IsAssociatedFunction Self "from_u8_unchecked" from_u8_unchecked.
      
      (*
          pub const fn digit(d: u8) -> Option<Self> {
              if d < 10 {
                  // SAFETY: Just checked it's in-range.
                  Some(unsafe { Self::digit_unchecked(d) })
              } else {
                  None
              }
          }
      *)
      Definition digit (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ d ] =>
          ltac:(M.monadic
            (let d := M.alloc (| d |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.lt (| M.read (| d |), Value.Integer IntegerKind.U8 10 |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ascii::ascii_char::AsciiChar",
                                "digit_unchecked",
                                []
                              |),
                              [ M.read (| d |) ]
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_digit : M.IsAssociatedFunction Self "digit" digit.
      
      (*
          pub const unsafe fn digit_unchecked(d: u8) -> Self {
              assert_unsafe_precondition!(
                  check_language_ub,
                  "`AsciiChar::digit_unchecked` input cannot exceed 9.",
                  (d: u8 = d) => d < 10
              );
      
              // SAFETY: `'0'` through `'9'` are U+00030 through U+0039,
              // so because `d` must be 64 or less the addition can return at most
              // 112 (0x70), which doesn't overflow and is within the ASCII range.
              unsafe {
                  let byte = b'0'.unchecked_add(d);
                  Self::from_u8_unchecked(byte)
              }
          }
      *)
      Definition digit_unchecked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ d ] =>
          ltac:(M.monadic
            (let d := M.alloc (| d |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_function (| "core::ub_checks::check_language_ub", [] |),
                                []
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Self,
                                "precondition_check.digit_unchecked",
                                []
                              |),
                              [ M.read (| d |) ]
                            |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ byte :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "u8", "unchecked_add", [] |),
                    [ M.read (| UnsupportedLiteral |); M.read (| d |) ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::ascii::ascii_char::AsciiChar",
                    "from_u8_unchecked",
                    []
                  |),
                  [ M.read (| byte |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_digit_unchecked :
        M.IsAssociatedFunction Self "digit_unchecked" digit_unchecked.
      
      (*
          pub const fn to_u8(self) -> u8 {
              self as u8
          }
      *)
      Definition to_u8 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.rust_cast (M.read (| self |))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_to_u8 : M.IsAssociatedFunction Self "to_u8" to_u8.
      
      (*
          pub const fn to_char(self) -> char {
              self as u8 as char
          }
      *)
      Definition to_char (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.rust_cast (M.rust_cast (M.read (| self |)))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_to_char : M.IsAssociatedFunction Self "to_char" to_char.
      
      (*
          pub const fn as_str(&self) -> &str {
              crate::slice::from_ref(self).as_str()
          }
      *)
      Definition as_str (ε : 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.apply (Ty.path "slice") [] [ Ty.path "core::ascii::ascii_char::AsciiChar" ],
                "as_str",
                []
              |),
              [
                M.call_closure (|
                  M.get_function (|
                    "core::slice::raw::from_ref",
                    [ Ty.path "core::ascii::ascii_char::AsciiChar" ]
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_str : M.IsAssociatedFunction Self "as_str" as_str.
    End Impl_core_ascii_ascii_char_AsciiChar.
    
    Module Impl_core_convert_From_core_ascii_ascii_char_AsciiChar_for_u8.
      Definition Self : Ty.t := Ty.path "u8".
      
      (*
                      fn from(chr: AsciiChar) -> $ty {
                          chr as u8 as $ty
                      }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ chr ] =>
          ltac:(M.monadic
            (let chr := M.alloc (| chr |) in
            M.read (| M.use (M.alloc (| M.rust_cast (M.read (| chr |)) |)) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "core::ascii::ascii_char::AsciiChar" ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_core_ascii_ascii_char_AsciiChar_for_u8.
    
    Module Impl_core_convert_From_core_ascii_ascii_char_AsciiChar_for_u16.
      Definition Self : Ty.t := Ty.path "u16".
      
      (*
                      fn from(chr: AsciiChar) -> $ty {
                          chr as u8 as $ty
                      }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ chr ] =>
          ltac:(M.monadic
            (let chr := M.alloc (| chr |) in
            M.rust_cast (M.rust_cast (M.read (| chr |)))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "core::ascii::ascii_char::AsciiChar" ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_core_ascii_ascii_char_AsciiChar_for_u16.
    
    Module Impl_core_convert_From_core_ascii_ascii_char_AsciiChar_for_u32.
      Definition Self : Ty.t := Ty.path "u32".
      
      (*
                      fn from(chr: AsciiChar) -> $ty {
                          chr as u8 as $ty
                      }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ chr ] =>
          ltac:(M.monadic
            (let chr := M.alloc (| chr |) in
            M.rust_cast (M.rust_cast (M.read (| chr |)))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "core::ascii::ascii_char::AsciiChar" ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_core_ascii_ascii_char_AsciiChar_for_u32.
    
    Module Impl_core_convert_From_core_ascii_ascii_char_AsciiChar_for_u64.
      Definition Self : Ty.t := Ty.path "u64".
      
      (*
                      fn from(chr: AsciiChar) -> $ty {
                          chr as u8 as $ty
                      }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ chr ] =>
          ltac:(M.monadic
            (let chr := M.alloc (| chr |) in
            M.rust_cast (M.rust_cast (M.read (| chr |)))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "core::ascii::ascii_char::AsciiChar" ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_core_ascii_ascii_char_AsciiChar_for_u64.
    
    Module Impl_core_convert_From_core_ascii_ascii_char_AsciiChar_for_u128.
      Definition Self : Ty.t := Ty.path "u128".
      
      (*
                      fn from(chr: AsciiChar) -> $ty {
                          chr as u8 as $ty
                      }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ chr ] =>
          ltac:(M.monadic
            (let chr := M.alloc (| chr |) in
            M.rust_cast (M.rust_cast (M.read (| chr |)))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "core::ascii::ascii_char::AsciiChar" ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_core_ascii_ascii_char_AsciiChar_for_u128.
    
    Module Impl_core_convert_From_core_ascii_ascii_char_AsciiChar_for_char.
      Definition Self : Ty.t := Ty.path "char".
      
      (*
                      fn from(chr: AsciiChar) -> $ty {
                          chr as u8 as $ty
                      }
      *)
      Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ chr ] =>
          ltac:(M.monadic
            (let chr := M.alloc (| chr |) in
            M.rust_cast (M.rust_cast (M.read (| chr |)))))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::From"
          Self
          (* Trait polymorphic types *) [ (* T *) Ty.path "core::ascii::ascii_char::AsciiChar" ]
          (* Instance *) [ ("from", InstanceField.Method from) ].
    End Impl_core_convert_From_core_ascii_ascii_char_AsciiChar_for_char.
    
    Module Impl_slice_core_ascii_ascii_char_AsciiChar.
      Definition Self : Ty.t :=
        Ty.apply (Ty.path "slice") [] [ Ty.path "core::ascii::ascii_char::AsciiChar" ].
      
      (*
          pub const fn as_str(&self) -> &str {
              let ascii_ptr: *const Self = self;
              let str_ptr = ascii_ptr as *const str;
              // SAFETY: Each ASCII codepoint in UTF-8 is encoded as one single-byte
              // code unit having the same value as the ASCII byte.
              unsafe { &*str_ptr }
          }
      *)
      Definition as_str (ε : 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~ ascii_ptr := M.alloc (| M.read (| self |) |) in
              let~ str_ptr := M.alloc (| M.rust_cast (M.read (| ascii_ptr |)) |) in
              M.alloc (| M.read (| str_ptr |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_str : M.IsAssociatedFunction Self "as_str" as_str.
      
      (*
          pub const fn as_bytes(&self) -> &[u8] {
              self.as_str().as_bytes()
          }
      *)
      Definition as_bytes (ε : 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 "str", "as_bytes", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "core::ascii::ascii_char::AsciiChar" ],
                    "as_str",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_as_bytes : M.IsAssociatedFunction Self "as_bytes" as_bytes.
    End Impl_slice_core_ascii_ascii_char_AsciiChar.
    
    Module Impl_core_fmt_Display_for_core_ascii_ascii_char_AsciiChar.
      Definition Self : Ty.t := Ty.path "core::ascii::ascii_char::AsciiChar".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              <str as fmt::Display>::fmt(self.as_str(), f)
          }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_trait_method (| "core::fmt::Display", Ty.path "str", [], "fmt", [] |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "core::ascii::ascii_char::AsciiChar",
                    "as_str",
                    []
                  |),
                  [ M.read (| self |) ]
                |);
                M.read (| f |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Display"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Display_for_core_ascii_ascii_char_AsciiChar.
    
    Module Impl_core_fmt_Debug_for_core_ascii_ascii_char_AsciiChar.
      Definition Self : Ty.t := Ty.path "core::ascii::ascii_char::AsciiChar".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              use AsciiChar::{Apostrophe, Null, ReverseSolidus as Backslash};
      
              fn backslash(a: AsciiChar) -> ([AsciiChar; 6], usize) {
                  ([Apostrophe, Backslash, a, Apostrophe, Null, Null], 4)
              }
      
              let (buf, len) = match self {
                  AsciiChar::Null => backslash(AsciiChar::Digit0),
                  AsciiChar::CharacterTabulation => backslash(AsciiChar::SmallT),
                  AsciiChar::CarriageReturn => backslash(AsciiChar::SmallR),
                  AsciiChar::LineFeed => backslash(AsciiChar::SmallN),
                  AsciiChar::ReverseSolidus => backslash(AsciiChar::ReverseSolidus),
                  AsciiChar::Apostrophe => backslash(AsciiChar::Apostrophe),
                  _ if self.to_u8().is_ascii_control() => {
                      const HEX_DIGITS: [AsciiChar; 16] = *b"0123456789abcdef".as_ascii().unwrap();
      
                      let byte = self.to_u8();
                      let hi = HEX_DIGITS[usize::from(byte >> 4)];
                      let lo = HEX_DIGITS[usize::from(byte & 0xf)];
                      ([Apostrophe, Backslash, AsciiChar::SmallX, hi, lo, Apostrophe], 6)
                  }
                  _ => ([Apostrophe, *self, Apostrophe, Null, Null, Null], 3),
              };
      
              f.write_str(buf[..len].as_str())
          }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.read (|
              M.match_operator (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (| γ, "core::ascii::ascii_char::AsciiChar::Null" |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (| Self, "backslash.fmt", [] |),
                            [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::Digit0" [] ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "core::ascii::ascii_char::AsciiChar::CharacterTabulation"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (| Self, "backslash.fmt", [] |),
                            [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallT" [] ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "core::ascii::ascii_char::AsciiChar::CarriageReturn"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (| Self, "backslash.fmt", [] |),
                            [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallR" [] ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "core::ascii::ascii_char::AsciiChar::LineFeed"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (| Self, "backslash.fmt", [] |),
                            [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallN" [] ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "core::ascii::ascii_char::AsciiChar::ReverseSolidus"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (| Self, "backslash.fmt", [] |),
                            [
                              Value.StructTuple
                                "core::ascii::ascii_char::AsciiChar::ReverseSolidus"
                                []
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "core::ascii::ascii_char::AsciiChar::Apostrophe"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (| Self, "backslash.fmt", [] |),
                            [ Value.StructTuple "core::ascii::ascii_char::AsciiChar::Apostrophe" []
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (| Ty.path "u8", "is_ascii_control", [] |),
                              [
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::ascii::ascii_char::AsciiChar",
                                      "to_u8",
                                      []
                                    |),
                                    [ M.read (| M.read (| self |) |) ]
                                  |)
                                |)
                              ]
                            |)
                          |) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ byte :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::ascii::ascii_char::AsciiChar",
                                "to_u8",
                                []
                              |),
                              [ M.read (| M.read (| self |) |) ]
                            |)
                          |) in
                        let~ hi :=
                          M.copy (|
                            M.SubPointer.get_array_field (|
                              M.get_constant (| "core::ascii::ascii_char::fmt::HEX_DIGITS" |),
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::From",
                                    Ty.path "usize",
                                    [ Ty.path "u8" ],
                                    "from",
                                    []
                                  |),
                                  [
                                    BinOp.Wrap.shr (|
                                      M.read (| byte |),
                                      Value.Integer IntegerKind.I32 4
                                    |)
                                  ]
                                |)
                              |)
                            |)
                          |) in
                        let~ lo :=
                          M.copy (|
                            M.SubPointer.get_array_field (|
                              M.get_constant (| "core::ascii::ascii_char::fmt::HEX_DIGITS" |),
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::From",
                                    Ty.path "usize",
                                    [ Ty.path "u8" ],
                                    "from",
                                    []
                                  |),
                                  [
                                    BinOp.bit_and
                                      (M.read (| byte |))
                                      (Value.Integer IntegerKind.U8 15)
                                  ]
                                |)
                              |)
                            |)
                          |) in
                        M.alloc (|
                          Value.Tuple
                            [
                              Value.Array
                                [
                                  Value.StructTuple
                                    "core::ascii::ascii_char::AsciiChar::Apostrophe"
                                    [];
                                  Value.StructTuple
                                    "core::ascii::ascii_char::AsciiChar::ReverseSolidus"
                                    [];
                                  Value.StructTuple "core::ascii::ascii_char::AsciiChar::SmallX" [];
                                  M.read (| hi |);
                                  M.read (| lo |);
                                  Value.StructTuple
                                    "core::ascii::ascii_char::AsciiChar::Apostrophe"
                                    []
                                ];
                              Value.Integer IntegerKind.Usize 6
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          Value.Tuple
                            [
                              Value.Array
                                [
                                  Value.StructTuple
                                    "core::ascii::ascii_char::AsciiChar::Apostrophe"
                                    [];
                                  M.read (| M.read (| self |) |);
                                  Value.StructTuple
                                    "core::ascii::ascii_char::AsciiChar::Apostrophe"
                                    [];
                                  Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [];
                                  Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [];
                                  Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" []
                                ];
                              Value.Integer IntegerKind.Usize 3
                            ]
                        |)))
                  ]
                |),
                [
                  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 buf := M.copy (| γ0_0 |) in
                      let len := M.copy (| γ0_1 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Formatter",
                            "write_str",
                            []
                          |),
                          [
                            M.read (| f |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "core::ascii::ascii_char::AsciiChar" ],
                                "as_str",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::index::Index",
                                    Ty.apply
                                      (Ty.path "array")
                                      [ Value.Integer IntegerKind.Usize 6 ]
                                      [ Ty.path "core::ascii::ascii_char::AsciiChar" ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::ops::range::RangeTo")
                                        []
                                        [ Ty.path "usize" ]
                                    ],
                                    "index",
                                    []
                                  |),
                                  [
                                    buf;
                                    Value.StructRecord
                                      "core::ops::range::RangeTo"
                                      [ ("end_", M.read (| len |)) ]
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_core_ascii_ascii_char_AsciiChar.
  End ascii_char.
End ascii.
