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

Module errmap.
  (* StructRecord
    {
      name := "ErrorDescription";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("code_name", Ty.path "alloc::string::String");
          ("code_description", Ty.path "alloc::string::String")
        ];
    } *)
  
  Module Impl_core_fmt_Debug_for_move_core_types_errmap_ErrorDescription.
    Definition Self : Ty.t := Ty.path "move_core_types::errmap::ErrorDescription".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field2_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "ErrorDescription" |);
              M.read (| Value.String "code_name" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_core_types::errmap::ErrorDescription",
                "code_name"
              |);
              M.read (| Value.String "code_description" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_core_types::errmap::ErrorDescription",
                  "code_description"
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_move_core_types_errmap_ErrorDescription.
  
  Module Impl_core_clone_Clone_for_move_core_types_errmap_ErrorDescription.
    Definition Self : Ty.t := Ty.path "move_core_types::errmap::ErrorDescription".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "move_core_types::errmap::ErrorDescription"
            [
              ("code_name",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "alloc::string::String",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_core_types::errmap::ErrorDescription",
                      "code_name"
                    |)
                  ]
                |));
              ("code_description",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "alloc::string::String",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_core_types::errmap::ErrorDescription",
                      "code_description"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => 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_move_core_types_errmap_ErrorDescription.
  
  Module underscore.
    Module Impl_serde_ser_Serialize_for_move_core_types_errmap_ErrorDescription.
      Definition Self : Ty.t := Ty.path "move_core_types::errmap::ErrorDescription".
      
      (* Serialize *)
      Definition serialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ __S ], [ self; __serializer ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let __serializer := M.alloc (| __serializer |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ __serde_state :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::Serializer",
                              __S,
                              [],
                              "serialize_struct",
                              []
                            |),
                            [
                              M.read (| __serializer |);
                              M.read (| Value.String "ErrorDescription" |);
                              BinOp.Wrap.add (|
                                BinOp.Wrap.add (|
                                  M.rust_cast (Value.Bool false),
                                  Value.Integer IntegerKind.Usize 1
                                |),
                                Value.Integer IntegerKind.Usize 1
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::result::Result::Ok",
                                  0
                                |) in
                              let __val := M.copy (| γ0_0 |) in
                              __val));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::result::Result::Err",
                                  0
                                |) in
                              let __err := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      Value.StructTuple
                                        "core::result::Result::Err"
                                        [ M.read (| __err |) ]
                                    |)
                                  |)
                                |)
                              |)))
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::SerializeStruct",
                            Ty.associated,
                            [],
                            "serialize_field",
                            [ Ty.path "alloc::string::String" ]
                          |),
                          [
                            __serde_state;
                            M.read (| Value.String "code_name" |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "move_core_types::errmap::ErrorDescription",
                              "code_name"
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Ok",
                                0
                              |) in
                            let __val := M.copy (| γ0_0 |) in
                            __val));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Err",
                                0
                              |) in
                            let __err := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Err"
                                      [ M.read (| __err |) ]
                                  |)
                                |)
                              |)
                            |)))
                      ]
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::SerializeStruct",
                            Ty.associated,
                            [],
                            "serialize_field",
                            [ Ty.path "alloc::string::String" ]
                          |),
                          [
                            __serde_state;
                            M.read (| Value.String "code_description" |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "move_core_types::errmap::ErrorDescription",
                              "code_description"
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Ok",
                                0
                              |) in
                            let __val := M.copy (| γ0_0 |) in
                            __val));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Err",
                                0
                              |) in
                            let __err := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Err"
                                      [ M.read (| __err |) ]
                                  |)
                                |)
                              |)
                            |)))
                      ]
                    |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "serde::ser::SerializeStruct",
                        Ty.associated,
                        [],
                        "end",
                        []
                      |),
                      [ M.read (| __serde_state |) ]
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "serde::ser::Serialize"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("serialize", InstanceField.Method serialize) ].
    End Impl_serde_ser_Serialize_for_move_core_types_errmap_ErrorDescription.
    Module Impl_serde_de_Deserialize_for_move_core_types_errmap_ErrorDescription.
      Definition Self : Ty.t := Ty.path "move_core_types::errmap::ErrorDescription".
      
      (* Deserialize *)
      Definition deserialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ __D ], [ __deserializer ] =>
          ltac:(M.monadic
            (let __deserializer := M.alloc (| __deserializer |) in
            M.call_closure (|
              M.get_trait_method (|
                "serde::de::Deserializer",
                __D,
                [],
                "deserialize_struct",
                [ Ty.path "move_core_types::errmap::_'1::deserialize::__Visitor" ]
              |),
              [
                M.read (| __deserializer |);
                M.read (| Value.String "ErrorDescription" |);
                M.read (|
                  M.get_constant (| "move_core_types::errmap::_'1::deserialize::FIELDS" |)
                |);
                Value.StructRecord
                  "move_core_types::errmap::_'1::deserialize::__Visitor"
                  [
                    ("marker", Value.StructTuple "core::marker::PhantomData" []);
                    ("lifetime", Value.StructTuple "core::marker::PhantomData" [])
                  ]
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "serde::de::Deserialize"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("deserialize", InstanceField.Method deserialize) ].
    End Impl_serde_de_Deserialize_for_move_core_types_errmap_ErrorDescription.
    Module Impl_serde_ser_Serialize_for_move_core_types_errmap_ErrorMapping.
      Definition Self : Ty.t := Ty.path "move_core_types::errmap::ErrorMapping".
      
      (* Serialize *)
      Definition serialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ __S ], [ self; __serializer ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let __serializer := M.alloc (| __serializer |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ __serde_state :=
                    M.copy (|
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::Serializer",
                              __S,
                              [],
                              "serialize_struct",
                              []
                            |),
                            [
                              M.read (| __serializer |);
                              M.read (| Value.String "ErrorMapping" |);
                              BinOp.Wrap.add (|
                                BinOp.Wrap.add (|
                                  M.rust_cast (Value.Bool false),
                                  Value.Integer IntegerKind.Usize 1
                                |),
                                Value.Integer IntegerKind.Usize 1
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::result::Result::Ok",
                                  0
                                |) in
                              let __val := M.copy (| γ0_0 |) in
                              __val));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::result::Result::Err",
                                  0
                                |) in
                              let __err := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      Value.StructTuple
                                        "core::result::Result::Err"
                                        [ M.read (| __err |) ]
                                    |)
                                  |)
                                |)
                              |)))
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::SerializeStruct",
                            Ty.associated,
                            [],
                            "serialize_field",
                            [
                              Ty.apply
                                (Ty.path "alloc::collections::btree::map::BTreeMap")
                                []
                                [
                                  Ty.path "u64";
                                  Ty.path "move_core_types::errmap::ErrorDescription";
                                  Ty.path "alloc::alloc::Global"
                                ]
                            ]
                          |),
                          [
                            __serde_state;
                            M.read (| Value.String "error_categories" |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "move_core_types::errmap::ErrorMapping",
                              "error_categories"
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Ok",
                                0
                              |) in
                            let __val := M.copy (| γ0_0 |) in
                            __val));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Err",
                                0
                              |) in
                            let __err := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Err"
                                      [ M.read (| __err |) ]
                                  |)
                                |)
                              |)
                            |)))
                      ]
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::SerializeStruct",
                            Ty.associated,
                            [],
                            "serialize_field",
                            [
                              Ty.apply
                                (Ty.path "alloc::collections::btree::map::BTreeMap")
                                []
                                [
                                  Ty.path "move_core_types::language_storage::ModuleId";
                                  Ty.apply
                                    (Ty.path "alloc::collections::btree::map::BTreeMap")
                                    []
                                    [
                                      Ty.path "u64";
                                      Ty.path "move_core_types::errmap::ErrorDescription";
                                      Ty.path "alloc::alloc::Global"
                                    ];
                                  Ty.path "alloc::alloc::Global"
                                ]
                            ]
                          |),
                          [
                            __serde_state;
                            M.read (| Value.String "module_error_maps" |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "move_core_types::errmap::ErrorMapping",
                              "module_error_maps"
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Ok",
                                0
                              |) in
                            let __val := M.copy (| γ0_0 |) in
                            __val));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::result::Result::Err",
                                0
                              |) in
                            let __err := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    Value.StructTuple
                                      "core::result::Result::Err"
                                      [ M.read (| __err |) ]
                                  |)
                                |)
                              |)
                            |)))
                      ]
                    |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "serde::ser::SerializeStruct",
                        Ty.associated,
                        [],
                        "end",
                        []
                      |),
                      [ M.read (| __serde_state |) ]
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "serde::ser::Serialize"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("serialize", InstanceField.Method serialize) ].
    End Impl_serde_ser_Serialize_for_move_core_types_errmap_ErrorMapping.
    Module Impl_serde_de_Deserialize_for_move_core_types_errmap_ErrorMapping.
      Definition Self : Ty.t := Ty.path "move_core_types::errmap::ErrorMapping".
      
      (* Deserialize *)
      Definition deserialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ __D ], [ __deserializer ] =>
          ltac:(M.monadic
            (let __deserializer := M.alloc (| __deserializer |) in
            M.call_closure (|
              M.get_trait_method (|
                "serde::de::Deserializer",
                __D,
                [],
                "deserialize_struct",
                [ Ty.path "move_core_types::errmap::_'3::deserialize::__Visitor" ]
              |),
              [
                M.read (| __deserializer |);
                M.read (| Value.String "ErrorMapping" |);
                M.read (|
                  M.get_constant (| "move_core_types::errmap::_'3::deserialize::FIELDS" |)
                |);
                Value.StructRecord
                  "move_core_types::errmap::_'3::deserialize::__Visitor"
                  [
                    ("marker", Value.StructTuple "core::marker::PhantomData" []);
                    ("lifetime", Value.StructTuple "core::marker::PhantomData" [])
                  ]
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "serde::de::Deserialize"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("deserialize", InstanceField.Method deserialize) ].
    End Impl_serde_de_Deserialize_for_move_core_types_errmap_ErrorMapping.
  End underscore.
  
  
  (* StructRecord
    {
      name := "ErrorMapping";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("error_categories",
            Ty.apply
              (Ty.path "alloc::collections::btree::map::BTreeMap")
              []
              [
                Ty.path "u64";
                Ty.path "move_core_types::errmap::ErrorDescription";
                Ty.path "alloc::alloc::Global"
              ]);
          ("module_error_maps",
            Ty.apply
              (Ty.path "alloc::collections::btree::map::BTreeMap")
              []
              [
                Ty.path "move_core_types::language_storage::ModuleId";
                Ty.apply
                  (Ty.path "alloc::collections::btree::map::BTreeMap")
                  []
                  [
                    Ty.path "u64";
                    Ty.path "move_core_types::errmap::ErrorDescription";
                    Ty.path "alloc::alloc::Global"
                  ];
                Ty.path "alloc::alloc::Global"
              ])
        ];
    } *)
  
  Module Impl_core_fmt_Debug_for_move_core_types_errmap_ErrorMapping.
    Definition Self : Ty.t := Ty.path "move_core_types::errmap::ErrorMapping".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field2_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "ErrorMapping" |);
              M.read (| Value.String "error_categories" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_core_types::errmap::ErrorMapping",
                "error_categories"
              |);
              M.read (| Value.String "module_error_maps" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_core_types::errmap::ErrorMapping",
                  "module_error_maps"
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_move_core_types_errmap_ErrorMapping.
  
  Module Impl_core_clone_Clone_for_move_core_types_errmap_ErrorMapping.
    Definition Self : Ty.t := Ty.path "move_core_types::errmap::ErrorMapping".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "move_core_types::errmap::ErrorMapping"
            [
              ("error_categories",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "alloc::collections::btree::map::BTreeMap")
                      []
                      [
                        Ty.path "u64";
                        Ty.path "move_core_types::errmap::ErrorDescription";
                        Ty.path "alloc::alloc::Global"
                      ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_core_types::errmap::ErrorMapping",
                      "error_categories"
                    |)
                  ]
                |));
              ("module_error_maps",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "alloc::collections::btree::map::BTreeMap")
                      []
                      [
                        Ty.path "move_core_types::language_storage::ModuleId";
                        Ty.apply
                          (Ty.path "alloc::collections::btree::map::BTreeMap")
                          []
                          [
                            Ty.path "u64";
                            Ty.path "move_core_types::errmap::ErrorDescription";
                            Ty.path "alloc::alloc::Global"
                          ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_core_types::errmap::ErrorMapping",
                      "module_error_maps"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => 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_move_core_types_errmap_ErrorMapping.
  
  
  
  Module Impl_core_default_Default_for_move_core_types_errmap_ErrorMapping.
    Definition Self : Ty.t := Ty.path "move_core_types::errmap::ErrorMapping".
    
    (* Default *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "move_core_types::errmap::ErrorMapping"
            [
              ("error_categories",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.apply
                      (Ty.path "alloc::collections::btree::map::BTreeMap")
                      []
                      [
                        Ty.path "u64";
                        Ty.path "move_core_types::errmap::ErrorDescription";
                        Ty.path "alloc::alloc::Global"
                      ],
                    [],
                    "default",
                    []
                  |),
                  []
                |));
              ("module_error_maps",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.apply
                      (Ty.path "alloc::collections::btree::map::BTreeMap")
                      []
                      [
                        Ty.path "move_core_types::language_storage::ModuleId";
                        Ty.apply
                          (Ty.path "alloc::collections::btree::map::BTreeMap")
                          []
                          [
                            Ty.path "u64";
                            Ty.path "move_core_types::errmap::ErrorDescription";
                            Ty.path "alloc::alloc::Global"
                          ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [],
                    "default",
                    []
                  |),
                  []
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::default::Default"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method default) ].
  End Impl_core_default_Default_for_move_core_types_errmap_ErrorMapping.
  
  Module Impl_move_core_types_errmap_ErrorMapping.
    Definition Self : Ty.t := Ty.path "move_core_types::errmap::ErrorMapping".
    
    (*
        pub fn add_error_category(
            &mut self,
            category_id: u64,
            description: ErrorDescription,
        ) -> Result<()> {
            if let Some(previous_entry) = self.error_categories.insert(category_id, description) {
                bail!(format!(
                    "Entry for category {} already taken by: {:#?}",
                    category_id, previous_entry
                ))
            }
            Ok(())
        }
    *)
    Definition add_error_category (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; category_id; description ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let category_id := M.alloc (| category_id |) in
          let description := M.alloc (| description |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::collections::btree::map::BTreeMap")
                                    []
                                    [
                                      Ty.path "u64";
                                      Ty.path "move_core_types::errmap::ErrorDescription";
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  "insert",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_core_types::errmap::ErrorMapping",
                                    "error_categories"
                                  |);
                                  M.read (| category_id |);
                                  M.read (| description |)
                                ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let previous_entry := M.copy (| γ0_0 |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      M.read (|
                                        let~ error :=
                                          M.copy (|
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::hint::must_use",
                                                    [ Ty.path "alloc::string::String" ]
                                                  |),
                                                  [
                                                    M.read (|
                                                      let~ res :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_function (|
                                                              "alloc::fmt::format",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.path "core::fmt::Arguments",
                                                                  "new_v1_formatted",
                                                                  []
                                                                |),
                                                                [
                                                                  M.alloc (|
                                                                    Value.Array
                                                                      [
                                                                        M.read (|
                                                                          Value.String
                                                                            "Entry for category "
                                                                        |);
                                                                        M.read (|
                                                                          Value.String
                                                                            " already taken by: "
                                                                        |)
                                                                      ]
                                                                  |);
                                                                  M.alloc (|
                                                                    Value.Array
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "core::fmt::rt::Argument",
                                                                            "new_display",
                                                                            [ Ty.path "u64" ]
                                                                          |),
                                                                          [ category_id ]
                                                                        |);
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "core::fmt::rt::Argument",
                                                                            "new_debug",
                                                                            [
                                                                              Ty.path
                                                                                "move_core_types::errmap::ErrorDescription"
                                                                            ]
                                                                          |),
                                                                          [ previous_entry ]
                                                                        |)
                                                                      ]
                                                                  |);
                                                                  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
                                                                              4;
                                                                            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",
                                                                      []
                                                                    |),
                                                                    []
                                                                  |)
                                                                ]
                                                              |)
                                                            ]
                                                          |)
                                                        |) in
                                                      res
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let error := M.copy (| γ |) in
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "anyhow::kind::Adhoc",
                                                          "new",
                                                          [ Ty.path "alloc::string::String" ]
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "anyhow::kind::AdhocKind",
                                                              Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [ Ty.path "alloc::string::String" ],
                                                              [],
                                                              "anyhow_kind",
                                                              []
                                                            |),
                                                            [ M.alloc (| error |) ]
                                                          |);
                                                          M.read (| error |)
                                                        ]
                                                      |)
                                                    |)))
                                              ]
                                            |)
                                          |) in
                                        error
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_add_error_category :
      M.IsAssociatedFunction Self "add_error_category" add_error_category.
    
    (*
        pub fn add_module_error(
            &mut self,
            module_id: ModuleId,
            abort_code: u64,
            description: ErrorDescription,
        ) -> Result<()> {
            let module_error_map = self.module_error_maps.entry(module_id.clone()).or_default();
            if let Some(previous_entry) = module_error_map.insert(abort_code, description) {
                bail!(format!(
                    "Duplicate entry for abort code {} found in {}, previous entry: {:#?}",
                    abort_code, module_id, previous_entry
                ))
            }
            Ok(())
        }
    *)
    Definition add_module_error (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; module_id; abort_code; description ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let module_id := M.alloc (| module_id |) in
          let abort_code := M.alloc (| abort_code |) in
          let description := M.alloc (| description |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ module_error_map :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::map::entry::Entry")
                          []
                          [
                            Ty.path "move_core_types::language_storage::ModuleId";
                            Ty.apply
                              (Ty.path "alloc::collections::btree::map::BTreeMap")
                              []
                              [
                                Ty.path "u64";
                                Ty.path "move_core_types::errmap::ErrorDescription";
                                Ty.path "alloc::alloc::Global"
                              ];
                            Ty.path "alloc::alloc::Global"
                          ],
                        "or_default",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::collections::btree::map::BTreeMap")
                              []
                              [
                                Ty.path "move_core_types::language_storage::ModuleId";
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::BTreeMap")
                                  []
                                  [
                                    Ty.path "u64";
                                    Ty.path "move_core_types::errmap::ErrorDescription";
                                    Ty.path "alloc::alloc::Global"
                                  ];
                                Ty.path "alloc::alloc::Global"
                              ],
                            "entry",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "move_core_types::errmap::ErrorMapping",
                              "module_error_maps"
                            |);
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::clone::Clone",
                                Ty.path "move_core_types::language_storage::ModuleId",
                                [],
                                "clone",
                                []
                              |),
                              [ module_id ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::collections::btree::map::BTreeMap")
                                    []
                                    [
                                      Ty.path "u64";
                                      Ty.path "move_core_types::errmap::ErrorDescription";
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  "insert",
                                  []
                                |),
                                [
                                  M.read (| module_error_map |);
                                  M.read (| abort_code |);
                                  M.read (| description |)
                                ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let previous_entry := M.copy (| γ0_0 |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      M.read (|
                                        let~ error :=
                                          M.copy (|
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::hint::must_use",
                                                    [ Ty.path "alloc::string::String" ]
                                                  |),
                                                  [
                                                    M.read (|
                                                      let~ res :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_function (|
                                                              "alloc::fmt::format",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.path "core::fmt::Arguments",
                                                                  "new_v1_formatted",
                                                                  []
                                                                |),
                                                                [
                                                                  M.alloc (|
                                                                    Value.Array
                                                                      [
                                                                        M.read (|
                                                                          Value.String
                                                                            "Duplicate entry for abort code "
                                                                        |);
                                                                        M.read (|
                                                                          Value.String " found in "
                                                                        |);
                                                                        M.read (|
                                                                          Value.String
                                                                            ", previous entry: "
                                                                        |)
                                                                      ]
                                                                  |);
                                                                  M.alloc (|
                                                                    Value.Array
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "core::fmt::rt::Argument",
                                                                            "new_display",
                                                                            [ Ty.path "u64" ]
                                                                          |),
                                                                          [ abort_code ]
                                                                        |);
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "core::fmt::rt::Argument",
                                                                            "new_display",
                                                                            [
                                                                              Ty.path
                                                                                "move_core_types::language_storage::ModuleId"
                                                                            ]
                                                                          |),
                                                                          [ module_id ]
                                                                        |);
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "core::fmt::rt::Argument",
                                                                            "new_debug",
                                                                            [
                                                                              Ty.path
                                                                                "move_core_types::errmap::ErrorDescription"
                                                                            ]
                                                                          |),
                                                                          [ previous_entry ]
                                                                        |)
                                                                      ]
                                                                  |);
                                                                  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
                                                                              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
                                                                              2;
                                                                            Value.UnicodeChar 32;
                                                                            Value.StructTuple
                                                                              "core::fmt::rt::Alignment::Unknown"
                                                                              [];
                                                                            Value.Integer
                                                                              IntegerKind.U32
                                                                              4;
                                                                            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",
                                                                      []
                                                                    |),
                                                                    []
                                                                  |)
                                                                ]
                                                              |)
                                                            ]
                                                          |)
                                                        |) in
                                                      res
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let error := M.copy (| γ |) in
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "anyhow::kind::Adhoc",
                                                          "new",
                                                          [ Ty.path "alloc::string::String" ]
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "anyhow::kind::AdhocKind",
                                                              Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [ Ty.path "alloc::string::String" ],
                                                              [],
                                                              "anyhow_kind",
                                                              []
                                                            |),
                                                            [ M.alloc (| error |) ]
                                                          |);
                                                          M.read (| error |)
                                                        ]
                                                      |)
                                                    |)))
                                              ]
                                            |)
                                          |) in
                                        error
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_add_module_error :
      M.IsAssociatedFunction Self "add_module_error" add_module_error.
    
    (*
        pub fn from_file<P: AsRef<Path>>(path: P) -> Self {
            let mut bytes = Vec::new();
            File::open(path).unwrap().read_to_end(&mut bytes).unwrap();
            bcs::from_bytes(&bytes).unwrap()
        }
    *)
    Definition from_file (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ P ], [ path ] =>
        ltac:(M.monadic
          (let path := M.alloc (| path |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                    "new",
                    []
                  |),
                  []
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::result::Result")
                      []
                      [ Ty.path "usize"; Ty.path "std::io::error::Error" ],
                    "unwrap",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "std::io::Read",
                        Ty.path "std::fs::File",
                        [],
                        "read_to_end",
                        []
                      |),
                      [
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [ Ty.path "std::fs::File"; Ty.path "std::io::error::Error" ],
                              "unwrap",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "std::fs::File",
                                  "open",
                                  [ P ]
                                |),
                                [ M.read (| path |) ]
                              |)
                            ]
                          |)
                        |);
                        bytes
                      ]
                    |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::result::Result")
                    []
                    [ Ty.path "move_core_types::errmap::ErrorMapping"; Ty.path "bcs::error::Error"
                    ],
                  "unwrap",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_function (|
                      "bcs::de::from_bytes",
                      [ Ty.path "move_core_types::errmap::ErrorMapping" ]
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::deref::Deref",
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                          [],
                          "deref",
                          []
                        |),
                        [ bytes ]
                      |)
                    ]
                  |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_file : M.IsAssociatedFunction Self "from_file" from_file.
    
    (*
        pub fn to_file<P: AsRef<Path>>(&self, path: P) {
            let bytes = bcs::to_bytes(self).unwrap();
            let mut file = File::create(path).unwrap();
            file.write_all(&bytes).unwrap();
        }
    *)
    Definition to_file (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ P ], [ self; path ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let path := M.alloc (| path |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::result::Result")
                      []
                      [
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ];
                        Ty.path "bcs::error::Error"
                      ],
                    "unwrap",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_function (|
                        "bcs::ser::to_bytes",
                        [ Ty.path "move_core_types::errmap::ErrorMapping" ]
                      |),
                      [ M.read (| self |) ]
                    |)
                  ]
                |)
              |) in
            let~ file :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::result::Result")
                      []
                      [ Ty.path "std::fs::File"; Ty.path "std::io::error::Error" ],
                    "unwrap",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "std::fs::File", "create", [ P ] |),
                      [ M.read (| path |) ]
                    |)
                  ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::result::Result")
                      []
                      [ Ty.tuple []; Ty.path "std::io::error::Error" ],
                    "unwrap",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "std::io::Write",
                        Ty.path "std::fs::File",
                        [],
                        "write_all",
                        []
                      |),
                      [
                        file;
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::Deref",
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                            [],
                            "deref",
                            []
                          |),
                          [ bytes ]
                        |)
                      ]
                    |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_file : M.IsAssociatedFunction Self "to_file" to_file.
    
    (*
        pub fn get_explanation(&self, module: &ModuleId, output_code: u64) -> Option<ErrorDescription> {
            self.module_error_maps
                .get(module)
                .and_then(|module_map| module_map.get(&output_code).cloned())
        }
    *)
    Definition get_explanation (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; module; output_code ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let module := M.alloc (| module |) in
          let output_code := M.alloc (| output_code |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [
                  Ty.apply
                    (Ty.path "&")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloc::collections::btree::map::BTreeMap")
                        []
                        [
                          Ty.path "u64";
                          Ty.path "move_core_types::errmap::ErrorDescription";
                          Ty.path "alloc::alloc::Global"
                        ]
                    ]
                ],
              "and_then",
              [
                Ty.path "move_core_types::errmap::ErrorDescription";
                Ty.function
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloc::collections::btree::map::BTreeMap")
                              []
                              [
                                Ty.path "u64";
                                Ty.path "move_core_types::errmap::ErrorDescription";
                                Ty.path "alloc::alloc::Global"
                              ]
                          ]
                      ]
                  ]
                  (Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [ Ty.path "move_core_types::errmap::ErrorDescription" ])
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::collections::btree::map::BTreeMap")
                    []
                    [
                      Ty.path "move_core_types::language_storage::ModuleId";
                      Ty.apply
                        (Ty.path "alloc::collections::btree::map::BTreeMap")
                        []
                        [
                          Ty.path "u64";
                          Ty.path "move_core_types::errmap::ErrorDescription";
                          Ty.path "alloc::alloc::Global"
                        ];
                      Ty.path "alloc::alloc::Global"
                    ],
                  "get",
                  [ Ty.path "move_core_types::language_storage::ModuleId" ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "move_core_types::errmap::ErrorMapping",
                    "module_error_maps"
                  |);
                  M.read (| module |)
                ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let module_map := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::option::Option")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [ Ty.path "move_core_types::errmap::ErrorDescription" ]
                                      ],
                                    "cloned",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::collections::btree::map::BTreeMap")
                                          []
                                          [
                                            Ty.path "u64";
                                            Ty.path "move_core_types::errmap::ErrorDescription";
                                            Ty.path "alloc::alloc::Global"
                                          ],
                                        "get",
                                        [ Ty.path "u64" ]
                                      |),
                                      [ M.read (| module_map |); output_code ]
                                    |)
                                  ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_explanation :
      M.IsAssociatedFunction Self "get_explanation" get_explanation.
  End Impl_move_core_types_errmap_ErrorMapping.
End errmap.
