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

Module option.
  (*
  Enum Option
  {
    const_params := [];
    ty_params := [ "T" ];
    variants :=
      [
        {
          name := "None";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Some";
          item := StructTuple [ T ];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_marker_Copy_where_core_marker_Copy_T_for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::Copy"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_where_core_marker_Copy_T_for_core_option_Option_T.
  
  Module Impl_core_cmp_Eq_where_core_cmp_Eq_T_for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::cmp::Eq"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method (assert_receiver_is_total_eq T)) ].
  End Impl_core_cmp_Eq_where_core_cmp_Eq_T_for_core_option_Option_T.
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    (* Debug *)
    Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "None" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Some" |); __self_0 ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_core_option_Option_T.
  
  Module Impl_core_hash_Hash_where_core_hash_Hash_T_for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    (* Hash *)
    Definition hash (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      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.apply (Ty.path "core::option::Option") [] [ T ] ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Ty.path "isize", [], "hash", [ __H ] |),
                  [ __self_discr; M.read (| state |) ]
                |)
              |) in
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "core::hash::Hash", T, [], "hash", [ __H ] |),
                        [ M.read (| __self_0 |); M.read (| state |) ]
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::hash::Hash"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method (hash T)) ].
  End Impl_core_hash_Hash_where_core_hash_Hash_T_for_core_option_Option_T.
  
  Module Impl_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    (*
        pub const fn is_some(&self) -> bool {
            matches!( *self, Some(_))
        }
    *)
    Definition is_some (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.read (| self |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    M.alloc (| Value.Bool true |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_some :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "is_some" (is_some T).
    
    (*
        pub fn is_some_and(self, f: impl FnOnce(T) -> bool) -> bool {
            match self {
                None => false,
                Some(x) => f(x),
            }
        }
    *)
    Definition is_some_and (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ impl_FnOnce_T__arrow_bool ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.Bool false |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let x := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          impl_FnOnce_T__arrow_bool,
                          [ Ty.tuple [ T ] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| f |); Value.Tuple [ M.read (| x |) ] ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_some_and :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "is_some_and" (is_some_and T).
    
    (*
        pub const fn is_none(&self) -> bool {
            !self.is_some()
        }
    *)
    Definition is_none (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          UnOp.not (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "core::option::Option") [] [ T ],
                "is_some",
                []
              |),
              [ M.read (| self |) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_none :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "is_none" (is_none T).
    
    (*
        pub fn is_none_or(self, f: impl FnOnce(T) -> bool) -> bool {
            match self {
                None => true,
                Some(x) => f(x),
            }
        }
    *)
    Definition is_none_or (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ impl_FnOnce_T__arrow_bool ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.Bool true |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let x := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          impl_FnOnce_T__arrow_bool,
                          [ Ty.tuple [ T ] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| f |); Value.Tuple [ M.read (| x |) ] ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_none_or :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "is_none_or" (is_none_or T).
    
    (*
        pub const fn as_ref(&self) -> Option<&T> {
            match *self {
                Some(ref x) => Some(x),
                None => None,
            }
        }
    *)
    Definition as_ref (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.read (| self |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let x := M.alloc (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple "core::option::Option::Some" [ M.read (| x |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_ref :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "as_ref" (as_ref T).
    
    (*
        pub const fn as_mut(&mut self) -> Option<&mut T> {
            match *self {
                Some(ref mut x) => Some(x),
                None => None,
            }
        }
    *)
    Definition as_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.read (| self |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let x := M.alloc (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple "core::option::Option::Some" [ M.read (| x |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "as_mut" (as_mut T).
    
    (*
        pub const fn as_pin_ref(self: Pin<&Self>) -> Option<Pin<&T>> {
            // FIXME(const-hack): use `map` once that is possible
            match Pin::get_ref(self).as_ref() {
                // SAFETY: `x` is guaranteed to be pinned because it comes from `self`
                // which is pinned.
                Some(x) => unsafe { Some(Pin::new_unchecked(x)) },
                None => None,
            }
        }
    *)
    Definition as_pin_ref (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::option::Option") [] [ T ],
                    "as_ref",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::pin::Pin")
                          []
                          [
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ]
                          ],
                        "get_ref",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let x := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::pin::Pin")
                                []
                                [ Ty.apply (Ty.path "&") [] [ T ] ],
                              "new_unchecked",
                              []
                            |),
                            [ M.read (| x |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_pin_ref :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "as_pin_ref" (as_pin_ref T).
    
    (*
        pub const fn as_pin_mut(self: Pin<&mut Self>) -> Option<Pin<&mut T>> {
            // SAFETY: `get_unchecked_mut` is never used to move the `Option` inside `self`.
            // `x` is guaranteed to be pinned because it comes from `self` which is pinned.
            unsafe {
                // FIXME(const-hack): use `map` once that is possible
                match Pin::get_unchecked_mut(self).as_mut() {
                    Some(x) => Some(Pin::new_unchecked(x)),
                    None => None,
                }
            }
        }
    *)
    Definition as_pin_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::option::Option") [] [ T ],
                    "as_mut",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::pin::Pin")
                          []
                          [
                            Ty.apply
                              (Ty.path "&mut")
                              []
                              [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ]
                          ],
                        "get_unchecked_mut",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let x := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::pin::Pin")
                                []
                                [ Ty.apply (Ty.path "&mut") [] [ T ] ],
                              "new_unchecked",
                              []
                            |),
                            [ M.read (| x |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_pin_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "as_pin_mut" (as_pin_mut T).
    
    (*
        const fn len(&self) -> usize {
            // Using the intrinsic avoids emitting a branch to get the 0 or 1.
            let discriminant: isize = crate::intrinsics::discriminant_value(self);
            discriminant as usize
        }
    *)
    Definition len (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ discriminant :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            M.alloc (| M.rust_cast (M.read (| discriminant |)) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_len : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "len" (len T).
    
    (*
        pub const fn as_slice(&self) -> &[T] {
            // SAFETY: When the `Option` is `Some`, we're using the actual pointer
            // to the payload, with a length of 1, so this is equivalent to
            // `slice::from_ref`, and thus is safe.
            // When the `Option` is `None`, the length used is 0, so to be safe it
            // just needs to be aligned, which it is because `&self` is aligned and
            // the offset used is a multiple of alignment.
            //
            // In the new version, the intrinsic always returns a pointer to an
            // in-bounds and correctly aligned position for a `T` (even if in the
            // `None` case it's just padding).
            unsafe {
                slice::from_raw_parts(
                    (self as *const Self).byte_add(core::mem::offset_of!(Self, Some.0)).cast(),
                    self.len(),
                )
            }
        }
    *)
    Definition as_slice (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_function (| "core::slice::raw::from_raw_parts", [ T ] |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "*const")
                    []
                    [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ],
                  "cast",
                  [ T ]
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "*const")
                        []
                        [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ],
                      "byte_add",
                      []
                    |),
                    [
                      M.read (| M.use (M.alloc (| M.read (| self |) |)) |);
                      M.read (|
                        (* `OffsetOf` expression are not handled yet *) M.alloc (| Value.Tuple [] |)
                      |)
                    ]
                  |)
                ]
              |);
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::option::Option") [] [ T ],
                  "len",
                  []
                |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_slice :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "as_slice" (as_slice T).
    
    (*
        pub const fn as_mut_slice(&mut self) -> &mut [T] {
            // SAFETY: When the `Option` is `Some`, we're using the actual pointer
            // to the payload, with a length of 1, so this is equivalent to
            // `slice::from_mut`, and thus is safe.
            // When the `Option` is `None`, the length used is 0, so to be safe it
            // just needs to be aligned, which it is because `&self` is aligned and
            // the offset used is a multiple of alignment.
            //
            // In the new version, the intrinsic creates a `*const T` from a
            // mutable reference  so it is safe to cast back to a mutable pointer
            // here. As with `as_slice`, the intrinsic always returns a pointer to
            // an in-bounds and correctly aligned position for a `T` (even if in
            // the `None` case it's just padding).
            unsafe {
                slice::from_raw_parts_mut(
                    (self as *mut Self).byte_add(core::mem::offset_of!(Self, Some.0)).cast(),
                    self.len(),
                )
            }
        }
    *)
    Definition as_mut_slice (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_function (| "core::slice::raw::from_raw_parts_mut", [ T ] |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "*mut")
                    []
                    [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ],
                  "cast",
                  [ T ]
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "*mut")
                        []
                        [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ],
                      "byte_add",
                      []
                    |),
                    [
                      M.read (| M.use (M.alloc (| M.read (| self |) |)) |);
                      M.read (|
                        (* `OffsetOf` expression are not handled yet *) M.alloc (| Value.Tuple [] |)
                      |)
                    ]
                  |)
                ]
              |);
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::option::Option") [] [ T ],
                  "len",
                  []
                |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_mut_slice :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "as_mut_slice" (as_mut_slice T).
    
    (*
        pub const fn expect(self, msg: &str) -> T {
            match self {
                Some(val) => val,
                None => expect_failed(msg),
            }
        }
    *)
    Definition expect (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; msg ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let msg := M.alloc (| msg |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let val := M.copy (| γ0_0 |) in
                    val));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::option::expect_failed", [] |),
                          [ M.read (| msg |) ]
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_expect :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "expect" (expect T).
    
    (*
        pub const fn unwrap(self) -> T {
            match self {
                Some(val) => val,
                None => unwrap_failed(),
            }
        }
    *)
    Definition unwrap (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let val := M.copy (| γ0_0 |) in
                    val));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::option::unwrap_failed", [] |),
                          []
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unwrap :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "unwrap" (unwrap T).
    
    (*
        pub fn unwrap_or(self, default: T) -> T {
            match self {
                Some(x) => x,
                None => default,
            }
        }
    *)
    Definition unwrap_or (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; default ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let default := M.alloc (| default |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let x := M.copy (| γ0_0 |) in
                    x));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    default))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unwrap_or :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "unwrap_or" (unwrap_or T).
    
    (*
        pub fn unwrap_or_else<F>(self, f: F) -> T
        where
            F: FnOnce() -> T,
        {
            match self {
                Some(x) => x,
                None => f(),
            }
        }
    *)
    Definition unwrap_or_else
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ F ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let x := M.copy (| γ0_0 |) in
                    x));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          F,
                          [ Ty.tuple [] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| f |); Value.Tuple [] ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unwrap_or_else :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "unwrap_or_else" (unwrap_or_else T).
    
    (*
        pub fn unwrap_or_default(self) -> T
        where
            T: Default,
        {
            match self {
                Some(x) => x,
                None => T::default(),
            }
        }
    *)
    Definition unwrap_or_default
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let x := M.copy (| γ0_0 |) in
                    x));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                        []
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unwrap_or_default :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "unwrap_or_default" (unwrap_or_default T).
    
    (*
        pub const unsafe fn unwrap_unchecked(self) -> T {
            match self {
                Some(val) => val,
                // SAFETY: the safety contract must be upheld by the caller.
                None => unsafe { hint::unreachable_unchecked() },
            }
        }
    *)
    Definition unwrap_unchecked
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let val := M.copy (| γ0_0 |) in
                    val));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::hint::unreachable_unchecked", [] |),
                          []
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unwrap_unchecked :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "unwrap_unchecked" (unwrap_unchecked T).
    
    (*
        pub fn map<U, F>(self, f: F) -> Option<U>
        where
            F: FnOnce(T) -> U,
        {
            match self {
                Some(x) => Some(f(x)),
                None => None,
            }
        }
    *)
    Definition map (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U; F ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let x := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::function::FnOnce",
                              F,
                              [ Ty.tuple [ T ] ],
                              "call_once",
                              []
                            |),
                            [ M.read (| f |); Value.Tuple [ M.read (| x |) ] ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_map : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "map" (map T).
    
    (*
        pub fn inspect<F: FnOnce(&T)>(self, f: F) -> Self {
            if let Some(ref x) = self {
                f(x);
            }
    
            self
        }
    *)
    Definition inspect (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ F ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := self in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let x := M.alloc (| γ0_0 |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::function::FnOnce",
                              F,
                              [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ],
                              "call_once",
                              []
                            |),
                            [ M.read (| f |); Value.Tuple [ M.read (| x |) ] ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_inspect :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "inspect" (inspect T).
    
    (*
        pub fn map_or<U, F>(self, default: U, f: F) -> U
        where
            F: FnOnce(T) -> U,
        {
            match self {
                Some(t) => f(t),
                None => default,
            }
        }
    *)
    Definition map_or (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U; F ], [ self; default; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let default := M.alloc (| default |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let t := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          F,
                          [ Ty.tuple [ T ] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| f |); Value.Tuple [ M.read (| t |) ] ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    default))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_map_or :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "map_or" (map_or T).
    
    (*
        pub fn map_or_else<U, D, F>(self, default: D, f: F) -> U
        where
            D: FnOnce() -> U,
            F: FnOnce(T) -> U,
        {
            match self {
                Some(t) => f(t),
                None => default(),
            }
        }
    *)
    Definition map_or_else (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U; D; F ], [ self; default; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let default := M.alloc (| default |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let t := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          F,
                          [ Ty.tuple [ T ] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| f |); Value.Tuple [ M.read (| t |) ] ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          D,
                          [ Ty.tuple [] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| default |); Value.Tuple [] ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_map_or_else :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "map_or_else" (map_or_else T).
    
    (*
        pub fn ok_or<E>(self, err: E) -> Result<T, E> {
            match self {
                Some(v) => Ok(v),
                None => Err(err),
            }
        }
    *)
    Definition ok_or (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ E ], [ self; err ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let err := M.alloc (| err |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let v := M.copy (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| v |) ] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      Value.StructTuple "core::result::Result::Err" [ M.read (| err |) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_ok_or :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "ok_or" (ok_or T).
    
    (*
        pub fn ok_or_else<E, F>(self, err: F) -> Result<T, E>
        where
            F: FnOnce() -> E,
        {
            match self {
                Some(v) => Ok(v),
                None => Err(err()),
            }
        }
    *)
    Definition ok_or_else (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ E; F ], [ self; err ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let err := M.alloc (| err |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let v := M.copy (| γ0_0 |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| v |) ] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::function::FnOnce",
                              F,
                              [ Ty.tuple [] ],
                              "call_once",
                              []
                            |),
                            [ M.read (| err |); Value.Tuple [] ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_ok_or_else :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "ok_or_else" (ok_or_else T).
    
    (*
        pub fn as_deref(&self) -> Option<&T::Target>
        where
            T: Deref,
        {
            self.as_ref().map(|t| t.deref())
        }
    *)
    Definition as_deref (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&") [] [ T ] ],
              "map",
              [
                Ty.apply (Ty.path "&") [] [ Ty.associated ];
                Ty.function
                  [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ]
                  (Ty.apply (Ty.path "&") [] [ Ty.associated ])
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::option::Option") [] [ T ],
                  "as_ref",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let t := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::deref::Deref",
                                    T,
                                    [],
                                    "deref",
                                    []
                                  |),
                                  [ M.read (| t |) ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_deref :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "as_deref" (as_deref T).
    
    (*
        pub fn as_deref_mut(&mut self) -> Option<&mut T::Target>
        where
            T: DerefMut,
        {
            self.as_mut().map(|t| t.deref_mut())
        }
    *)
    Definition as_deref_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&mut") [] [ T ] ],
              "map",
              [
                Ty.apply (Ty.path "&mut") [] [ Ty.associated ];
                Ty.function
                  [ Ty.tuple [ Ty.apply (Ty.path "&mut") [] [ T ] ] ]
                  (Ty.apply (Ty.path "&mut") [] [ Ty.associated ])
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::option::Option") [] [ T ],
                  "as_mut",
                  []
                |),
                [ M.read (| self |) ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let t := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::deref::DerefMut",
                                    T,
                                    [],
                                    "deref_mut",
                                    []
                                  |),
                                  [ M.read (| t |) ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_as_deref_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "as_deref_mut" (as_deref_mut T).
    
    (*
        pub fn iter(&self) -> Iter<'_, T> {
            Iter { inner: Item { opt: self.as_ref() } }
        }
    *)
    Definition iter (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::option::Iter"
            [
              ("inner",
                Value.StructRecord
                  "core::option::Item"
                  [
                    ("opt",
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::option::Option") [] [ T ],
                          "as_ref",
                          []
                        |),
                        [ M.read (| self |) ]
                      |))
                  ])
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_iter :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "iter" (iter T).
    
    (*
        pub fn iter_mut(&mut self) -> IterMut<'_, T> {
            IterMut { inner: Item { opt: self.as_mut() } }
        }
    *)
    Definition iter_mut (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::option::IterMut"
            [
              ("inner",
                Value.StructRecord
                  "core::option::Item"
                  [
                    ("opt",
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::option::Option") [] [ T ],
                          "as_mut",
                          []
                        |),
                        [ M.read (| self |) ]
                      |))
                  ])
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_iter_mut :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "iter_mut" (iter_mut T).
    
    (*
        pub fn and<U>(self, optb: Option<U>) -> Option<U> {
            match self {
                Some(_) => optb,
                None => None,
            }
        }
    *)
    Definition and (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U ], [ self; optb ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let optb := M.alloc (| optb |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    optb));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_and : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "and" (and T).
    
    (*
        pub fn and_then<U, F>(self, f: F) -> Option<U>
        where
            F: FnOnce(T) -> Option<U>,
        {
            match self {
                Some(x) => f(x),
                None => None,
            }
        }
    *)
    Definition and_then (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U; F ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let x := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          F,
                          [ Ty.tuple [ T ] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| f |); Value.Tuple [ M.read (| x |) ] ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_and_then :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "and_then" (and_then T).
    
    (*
        pub fn filter<P>(self, predicate: P) -> Self
        where
            P: FnOnce(&T) -> bool,
        {
            if let Some(x) = self {
                if predicate(&x) {
                    return Some(x);
                }
            }
            None
        }
    *)
    Definition filter (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ P ], [ self; predicate ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let predicate := M.alloc (| predicate |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := self in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let x := M.copy (| γ0_0 |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::function::FnOnce",
                                            P,
                                            [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ T ] ] ],
                                            "call_once",
                                            []
                                          |),
                                          [ M.read (| predicate |); Value.Tuple [ x ] ]
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::option::Option::Some"
                                            [ M.read (| x |) ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_filter :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "filter" (filter T).
    
    (*
        pub fn or(self, optb: Option<T>) -> Option<T> {
            match self {
                x @ Some(_) => x,
                None => optb,
            }
        }
    *)
    Definition or (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; optb ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let optb := M.alloc (| optb |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let x := M.copy (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    x));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    optb))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_or : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "or" (or T).
    
    (*
        pub fn or_else<F>(self, f: F) -> Option<T>
        where
            F: FnOnce() -> Option<T>,
        {
            match self {
                x @ Some(_) => x,
                None => f(),
            }
        }
    *)
    Definition or_else (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ F ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let x := M.copy (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    x));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::function::FnOnce",
                          F,
                          [ Ty.tuple [] ],
                          "call_once",
                          []
                        |),
                        [ M.read (| f |); Value.Tuple [] ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_or_else :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "or_else" (or_else T).
    
    (*
        pub fn xor(self, optb: Option<T>) -> Option<T> {
            match (self, optb) {
                (a @ Some(_), None) => a,
                (None, b @ Some(_)) => b,
                _ => None,
            }
        }
    *)
    Definition xor (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; optb ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let optb := M.alloc (| optb |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [ M.read (| self |); M.read (| optb |) ] |),
              [
                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 a := M.copy (| γ0_0 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "core::option::Option::Some",
                        0
                      |) in
                    let _ := M.is_struct_tuple (| γ0_1, "core::option::Option::None" |) in
                    a));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let _ := M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                    let b := M.copy (| γ0_1 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_1,
                        "core::option::Option::Some",
                        0
                      |) in
                    b));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_xor : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "xor" (xor T).
    
    (*
        pub fn insert(&mut self, value: T) -> &mut T {
            *self = Some(value);
    
            // SAFETY: the code above just filled the option
            unsafe { self.as_mut().unwrap_unchecked() }
        }
    *)
    Definition insert (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; value ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let value := M.alloc (| value |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.read (| self |),
                Value.StructTuple "core::option::Option::Some" [ M.read (| value |) ]
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [ Ty.apply (Ty.path "&mut") [] [ T ] ],
                  "unwrap_unchecked",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::option::Option") [] [ T ],
                      "as_mut",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_insert :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "insert" (insert T).
    
    (*
        pub fn get_or_insert(&mut self, value: T) -> &mut T {
            self.get_or_insert_with(|| value)
        }
    *)
    Definition get_or_insert (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; value ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let value := M.alloc (| value |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ T ],
              "get_or_insert_with",
              [ Ty.function [ Ty.tuple [] ] T ]
            |),
            [
              M.read (| self |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [ fun γ => ltac:(M.monadic (M.read (| value |))) ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_or_insert :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "get_or_insert" (get_or_insert T).
    
    (*
        pub fn get_or_insert_default(&mut self) -> &mut T
        where
            T: Default,
        {
            self.get_or_insert_with(T::default)
        }
    *)
    Definition get_or_insert_default
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ T ],
              "get_or_insert_with",
              [ Ty.function [] T ]
            |),
            [
              M.read (| self |);
              M.get_trait_method (| "core::default::Default", T, [], "default", [] |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_or_insert_default :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "get_or_insert_default" (get_or_insert_default T).
    
    (*
        pub fn get_or_insert_with<F>(&mut self, f: F) -> &mut T
        where
            F: FnOnce() -> T,
        {
            if let None = self {
                *self = Some(f());
            }
    
            // SAFETY: a `None` variant for `self` would have been replaced by a `Some`
            // variant in the code above.
            unsafe { self.as_mut().unwrap_unchecked() }
        }
    *)
    Definition get_or_insert_with
        (T : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ F ], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := self in
                      let γ := M.read (| γ |) in
                      let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                      let~ _ :=
                        M.write (|
                          M.read (| self |),
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::function::FnOnce",
                                  F,
                                  [ Ty.tuple [] ],
                                  "call_once",
                                  []
                                |),
                                [ M.read (| f |); Value.Tuple [] ]
                              |)
                            ]
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [ Ty.apply (Ty.path "&mut") [] [ T ] ],
                  "unwrap_unchecked",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::option::Option") [] [ T ],
                      "as_mut",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_or_insert_with :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "get_or_insert_with" (get_or_insert_with T).
    
    (*
        pub const fn take(&mut self) -> Option<T> {
            // FIXME(const-hack) replace `mem::replace` by `mem::take` when the latter is const ready
            mem::replace(self, None)
        }
    *)
    Definition take (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_function (|
              "core::mem::replace",
              [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ]
            |),
            [ M.read (| self |); Value.StructTuple "core::option::Option::None" [] ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_take :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "take" (take T).
    
    (*
        pub fn take_if<P>(&mut self, predicate: P) -> Option<T>
        where
            P: FnOnce(&mut T) -> bool,
        {
            if self.as_mut().map_or(false, predicate) { self.take() } else { None }
        }
    *)
    Definition take_if (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ P ], [ self; predicate ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let predicate := M.alloc (| predicate |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::option::Option")
                                []
                                [ Ty.apply (Ty.path "&mut") [] [ T ] ],
                              "map_or",
                              [ Ty.path "bool"; P ]
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "core::option::Option") [] [ T ],
                                  "as_mut",
                                  []
                                |),
                                [ M.read (| self |) ]
                              |);
                              Value.Bool false;
                              M.read (| predicate |)
                            ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::option::Option") [] [ T ],
                          "take",
                          []
                        |),
                        [ M.read (| self |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_take_if :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "take_if" (take_if T).
    
    (*
        pub const fn replace(&mut self, value: T) -> Option<T> {
            mem::replace(self, Some(value))
        }
    *)
    Definition replace (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; value ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let value := M.alloc (| value |) in
          M.call_closure (|
            M.get_function (|
              "core::mem::replace",
              [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ]
            |),
            [
              M.read (| self |);
              Value.StructTuple "core::option::Option::Some" [ M.read (| value |) ]
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_replace :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "replace" (replace T).
    
    (*
        pub fn zip<U>(self, other: Option<U>) -> Option<(T, U)> {
            match (self, other) {
                (Some(a), Some(b)) => Some((a, b)),
                _ => None,
            }
        }
    *)
    Definition zip (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U ], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "core::option::Option::Some",
                        0
                      |) in
                    let a := M.copy (| γ1_0 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_1,
                        "core::option::Option::Some",
                        0
                      |) in
                    let b := M.copy (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [ Value.Tuple [ M.read (| a |); M.read (| b |) ] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_zip : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "zip" (zip T).
    
    (*
        pub fn zip_with<U, F, R>(self, other: Option<U>, f: F) -> Option<R>
        where
            F: FnOnce(T, U) -> R,
        {
            match (self, other) {
                (Some(a), Some(b)) => Some(f(a, b)),
                _ => None,
            }
        }
    *)
    Definition zip_with (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [ U; F; R ], [ self; other; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "core::option::Option::Some",
                        0
                      |) in
                    let a := M.copy (| γ1_0 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_1,
                        "core::option::Option::Some",
                        0
                      |) in
                    let b := M.copy (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::function::FnOnce",
                              F,
                              [ Ty.tuple [ T; U ] ],
                              "call_once",
                              []
                            |),
                            [ M.read (| f |); Value.Tuple [ M.read (| a |); M.read (| b |) ] ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_zip_with :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "zip_with" (zip_with T).
  End Impl_core_option_Option_T.
  
  Module Impl_core_option_Option_Tuple_T_U_.
    Definition Self (T U : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::option::Option") [] [ Ty.tuple [ T; U ] ].
    
    (*
        pub fn unzip(self) -> (Option<T>, Option<U>) {
            match self {
                Some((a, b)) => (Some(a), Some(b)),
                None => (None, None),
            }
        }
    *)
    Definition unzip (T U : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T U in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                    let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                    let a := M.copy (| γ1_0 |) in
                    let b := M.copy (| γ1_1 |) in
                    M.alloc (|
                      Value.Tuple
                        [
                          Value.StructTuple "core::option::Option::Some" [ M.read (| a |) ];
                          Value.StructTuple "core::option::Option::Some" [ M.read (| b |) ]
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      Value.Tuple
                        [
                          Value.StructTuple "core::option::Option::None" [];
                          Value.StructTuple "core::option::Option::None" []
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unzip :
      forall (T U : Ty.t),
      M.IsAssociatedFunction (Self T U) "unzip" (unzip T U).
  End Impl_core_option_Option_Tuple_T_U_.
  
  Module Impl_core_option_Option_ref__T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&") [] [ T ] ].
    
    (*
        pub const fn copied(self) -> Option<T>
        where
            T: Copy,
        {
            // FIXME(const-hack): this implementation, which sidesteps using `Option::map` since it's not const
            // ready yet, should be reverted when possible to avoid code repetition
            match self {
                Some(&v) => Some(v),
                None => None,
            }
        }
    *)
    Definition copied (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let γ0_0 := M.read (| γ0_0 |) in
                    let v := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple "core::option::Option::Some" [ M.read (| v |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_copied :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "copied" (copied T).
    
    (*
        pub fn cloned(self) -> Option<T>
        where
            T: Clone,
        {
            match self {
                Some(t) => Some(t.clone()),
                None => None,
            }
        }
    *)
    Definition cloned (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let t := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          M.call_closure (|
                            M.get_trait_method (| "core::clone::Clone", T, [], "clone", [] |),
                            [ M.read (| t |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_cloned :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "cloned" (cloned T).
  End Impl_core_option_Option_ref__T.
  
  Module Impl_core_option_Option_ref_mut_T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&mut") [] [ T ] ].
    
    (*
        pub const fn copied(self) -> Option<T>
        where
            T: Copy,
        {
            match self {
                Some(&mut t) => Some(t),
                None => None,
            }
        }
    *)
    Definition copied (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let γ0_0 := M.read (| γ0_0 |) in
                    let t := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple "core::option::Option::Some" [ M.read (| t |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_copied :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "copied" (copied T).
    
    (*
        pub fn cloned(self) -> Option<T>
        where
            T: Clone,
        {
            match self {
                Some(t) => Some(t.clone()),
                None => None,
            }
        }
    *)
    Definition cloned (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let t := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          M.call_closure (|
                            M.get_trait_method (| "core::clone::Clone", T, [], "clone", [] |),
                            [ M.read (| t |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_cloned :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "cloned" (cloned T).
  End Impl_core_option_Option_ref_mut_T.
  
  Module Impl_core_option_Option_core_result_Result_T_E.
    Definition Self (T E : Ty.t) : Ty.t :=
      Ty.apply
        (Ty.path "core::option::Option")
        []
        [ Ty.apply (Ty.path "core::result::Result") [] [ T; E ] ].
    
    (*
        pub const fn transpose(self) -> Result<Option<T>, E> {
            match self {
                Some(Ok(x)) => Ok(Some(x)),
                Some(Err(e)) => Err(e),
                None => Ok(None),
            }
        }
    *)
    Definition transpose (T E : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T E in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "core::result::Result::Ok",
                        0
                      |) in
                    let x := M.copy (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [ Value.StructTuple "core::option::Option::Some" [ M.read (| x |) ] ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "core::result::Result::Err",
                        0
                      |) in
                    let e := M.copy (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple "core::result::Result::Err" [ M.read (| e |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [ Value.StructTuple "core::option::Option::None" [] ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_transpose :
      forall (T E : Ty.t),
      M.IsAssociatedFunction (Self T E) "transpose" (transpose T E).
  End Impl_core_option_Option_core_result_Result_T_E.
  
  (*
  const fn unwrap_failed() -> ! {
      panic("called `Option::unwrap()` on a `None` value")
  }
  *)
  Definition unwrap_failed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_function (| "core::panicking::panic", [] |),
          [ M.read (| Value.String "called `Option::unwrap()` on a `None` value" |) ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_unwrap_failed : M.IsFunction "core::option::unwrap_failed" unwrap_failed.
  
  (*
  const fn expect_failed(msg: &str) -> ! {
      panic_display(&msg)
  }
  *)
  Definition expect_failed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ msg ] =>
      ltac:(M.monadic
        (let msg := M.alloc (| msg |) in
        M.call_closure (|
          M.get_function (|
            "core::panicking::panic_display",
            [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
          |),
          [ msg ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_expect_failed : M.IsFunction "core::option::expect_failed" expect_failed.
  
  Module Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    (*
        fn clone(&self) -> Self {
            match self {
                Some(x) => Some(x.clone()),
                None => None,
            }
        }
    *)
    Definition clone (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let x := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          M.call_closure (|
                            M.get_trait_method (| "core::clone::Clone", T, [], "clone", [] |),
                            [ M.read (| x |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn clone_from(&mut self, source: &Self) {
            match (self, source) {
                (Some(to), Some(from)) => to.clone_from(from),
                (to, from) => *to = from.clone(),
            }
        }
    *)
    Definition clone_from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; source ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let source := M.alloc (| source |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [ M.read (| self |); M.read (| source |) ] |),
              [
                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 γ0_0 := M.read (| γ0_0 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "core::option::Option::Some",
                        0
                      |) in
                    let to := M.alloc (| γ2_0 |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_1,
                        "core::option::Option::Some",
                        0
                      |) in
                    let from := M.alloc (| γ2_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "core::clone::Clone", T, [], "clone_from", [] |),
                        [ M.read (| to |); M.read (| from |) ]
                      |)
                    |)));
                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 to := M.copy (| γ0_0 |) in
                    let from := M.copy (| γ0_1 |) in
                    M.write (|
                      M.read (| to |),
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::clone::Clone",
                          Ty.apply (Ty.path "core::option::Option") [] [ T ],
                          [],
                          "clone",
                          []
                        |),
                        [ M.read (| from |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("clone", InstanceField.Method (clone T));
          ("clone_from", InstanceField.Method (clone_from T))
        ].
  End Impl_core_clone_Clone_where_core_clone_Clone_T_for_core_option_Option_T.
  
  Module Impl_core_default_Default_for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    (*
        fn default() -> Option<T> {
            None
        }
    *)
    Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [] => ltac:(M.monadic (Value.StructTuple "core::option::Option::None" []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::default::Default"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method (default T)) ].
  End Impl_core_default_Default_for_core_option_Option_T.
  
  Module Impl_core_iter_traits_collect_IntoIterator_for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    (*     type Item = T; *)
    Definition _Item (T : Ty.t) : Ty.t := T.
    
    (*     type IntoIter = IntoIter<T>; *)
    Definition _IntoIter (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IntoIter") [] [ T ].
    
    (*
        fn into_iter(self) -> IntoIter<T> {
            IntoIter { inner: Item { opt: self } }
        }
    *)
    Definition into_iter (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::option::IntoIter"
            [ ("inner", Value.StructRecord "core::option::Item" [ ("opt", M.read (| self |)) ]) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::collect::IntoIterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item T));
          ("IntoIter", InstanceField.Ty (_IntoIter T));
          ("into_iter", InstanceField.Method (into_iter T))
        ].
  End Impl_core_iter_traits_collect_IntoIterator_for_core_option_Option_T.
  
  Module Impl_core_iter_traits_collect_IntoIterator_for_ref__core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ].
    
    (*     type Item = &'a T; *)
    Definition _Item (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
    
    (*     type IntoIter = Iter<'a, T>; *)
    Definition _IntoIter (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Iter") [] [ T ].
    
    (*
        fn into_iter(self) -> Iter<'a, T> {
            self.iter()
        }
    *)
    Definition into_iter (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ T ],
              "iter",
              []
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::collect::IntoIterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item T));
          ("IntoIter", InstanceField.Ty (_IntoIter T));
          ("into_iter", InstanceField.Method (into_iter T))
        ].
  End Impl_core_iter_traits_collect_IntoIterator_for_ref__core_option_Option_T.
  
  Module Impl_core_iter_traits_collect_IntoIterator_for_ref_mut_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ].
    
    (*     type Item = &'a mut T; *)
    Definition _Item (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
    
    (*     type IntoIter = IterMut<'a, T>; *)
    Definition _IntoIter (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IterMut") [] [ T ].
    
    (*
        fn into_iter(self) -> IterMut<'a, T> {
            self.iter_mut()
        }
    *)
    Definition into_iter (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ T ],
              "iter_mut",
              []
            |),
            [ M.read (| self |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::collect::IntoIterator"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item T));
          ("IntoIter", InstanceField.Ty (_IntoIter T));
          ("into_iter", InstanceField.Method (into_iter T))
        ].
  End Impl_core_iter_traits_collect_IntoIterator_for_ref_mut_core_option_Option_T.
  
  Module Impl_core_convert_From_T_for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    (*
        fn from(val: T) -> Option<T> {
            Some(val)
        }
    *)
    Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ val ] =>
        ltac:(M.monadic
          (let val := M.alloc (| val |) in
          Value.StructTuple "core::option::Option::Some" [ M.read (| val |) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::convert::From"
        (Self T)
        (* Trait polymorphic types *) [ (* T *) T ]
        (* Instance *) [ ("from", InstanceField.Method (from T)) ].
  End Impl_core_convert_From_T_for_core_option_Option_T.
  
  Module Impl_core_convert_From_ref__core_option_Option_T_for_core_option_Option_ref__T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&") [] [ T ] ].
    
    (*
        fn from(o: &'a Option<T>) -> Option<&'a T> {
            o.as_ref()
        }
    *)
    Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ o ] =>
        ltac:(M.monadic
          (let o := M.alloc (| o |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ T ],
              "as_ref",
              []
            |),
            [ M.read (| o |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::convert::From"
        (Self T)
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ] ]
        (* Instance *) [ ("from", InstanceField.Method (from T)) ].
  End Impl_core_convert_From_ref__core_option_Option_T_for_core_option_Option_ref__T.
  
  Module Impl_core_convert_From_ref_mut_core_option_Option_T_for_core_option_Option_ref_mut_T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::option::Option") [] [ Ty.apply (Ty.path "&mut") [] [ T ] ].
    
    (*
        fn from(o: &'a mut Option<T>) -> Option<&'a mut T> {
            o.as_mut()
        }
    *)
    Definition from (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ o ] =>
        ltac:(M.monadic
          (let o := M.alloc (| o |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ T ],
              "as_mut",
              []
            |),
            [ M.read (| o |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::convert::From"
        (Self T)
        (* Trait polymorphic types *)
        [
          (* T *)
          Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ]
        ]
        (* Instance *) [ ("from", InstanceField.Method (from T)) ].
  End Impl_core_convert_From_ref_mut_core_option_Option_T_for_core_option_Option_ref_mut_T.
  
  Module Impl_core_marker_StructuralPartialEq_for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_core_option_Option_T.
  
  Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    (*
        fn eq(&self, other: &Self) -> bool {
            // Spelling out the cases explicitly optimizes better than
            // `_ => false`
            match (self, other) {
                (Some(l), Some(r)) => *l == *r,
                (Some(_), None) => false,
                (None, Some(_)) => false,
                (None, None) => true,
            }
        }
    *)
    Definition eq (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
              [
                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 γ0_0 := M.read (| γ0_0 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "core::option::Option::Some",
                        0
                      |) in
                    let l := M.alloc (| γ2_0 |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_1,
                        "core::option::Option::Some",
                        0
                      |) in
                    let r := M.alloc (| γ2_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "core::cmp::PartialEq", T, [ T ], "eq", [] |),
                        [ M.read (| l |); M.read (| r |) ]
                      |)
                    |)));
                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 γ0_0 := M.read (| γ0_0 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "core::option::Option::Some",
                        0
                      |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let _ := M.is_struct_tuple (| γ0_1, "core::option::Option::None" |) in
                    M.alloc (| Value.Bool false |)));
                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 γ0_0 := M.read (| γ0_0 |) in
                    let _ := M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_1,
                        "core::option::Option::Some",
                        0
                      |) in
                    M.alloc (| Value.Bool false |)));
                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 γ0_0 := M.read (| γ0_0 |) in
                    let _ := M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let _ := M.is_struct_tuple (| γ0_1, "core::option::Option::None" |) in
                    M.alloc (| Value.Bool true |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialEq"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method (eq T)) ].
  End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_T_for_core_option_Option_T.
  
  Module Impl_core_cmp_PartialOrd_where_core_cmp_PartialOrd_T_for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    (*
        fn partial_cmp(&self, other: &Self) -> Option<cmp::Ordering> {
            match (self, other) {
                (Some(l), Some(r)) => l.partial_cmp(r),
                (Some(_), None) => Some(cmp::Ordering::Greater),
                (None, Some(_)) => Some(cmp::Ordering::Less),
                (None, None) => Some(cmp::Ordering::Equal),
            }
        }
    *)
    Definition partial_cmp (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
              [
                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 γ0_0 := M.read (| γ0_0 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "core::option::Option::Some",
                        0
                      |) in
                    let l := M.alloc (| γ2_0 |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_1,
                        "core::option::Option::Some",
                        0
                      |) in
                    let r := M.alloc (| γ2_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialOrd",
                          T,
                          [ T ],
                          "partial_cmp",
                          []
                        |),
                        [ M.read (| l |); M.read (| r |) ]
                      |)
                    |)));
                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 γ0_0 := M.read (| γ0_0 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "core::option::Option::Some",
                        0
                      |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let _ := M.is_struct_tuple (| γ0_1, "core::option::Option::None" |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [ Value.StructTuple "core::cmp::Ordering::Greater" [] ]
                    |)));
                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 γ0_0 := M.read (| γ0_0 |) in
                    let _ := M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_1,
                        "core::option::Option::Some",
                        0
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [ Value.StructTuple "core::cmp::Ordering::Less" [] ]
                    |)));
                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 γ0_0 := M.read (| γ0_0 |) in
                    let _ := M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let _ := M.is_struct_tuple (| γ0_1, "core::option::Option::None" |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [ Value.StructTuple "core::cmp::Ordering::Equal" [] ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("partial_cmp", InstanceField.Method (partial_cmp T)) ].
  End Impl_core_cmp_PartialOrd_where_core_cmp_PartialOrd_T_for_core_option_Option_T.
  
  Module Impl_core_cmp_Ord_where_core_cmp_Ord_T_for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    (*
        fn cmp(&self, other: &Self) -> cmp::Ordering {
            match (self, other) {
                (Some(l), Some(r)) => l.cmp(r),
                (Some(_), None) => cmp::Ordering::Greater,
                (None, Some(_)) => cmp::Ordering::Less,
                (None, None) => cmp::Ordering::Equal,
            }
        }
    *)
    Definition cmp (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
              [
                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 γ0_0 := M.read (| γ0_0 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "core::option::Option::Some",
                        0
                      |) in
                    let l := M.alloc (| γ2_0 |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_1,
                        "core::option::Option::Some",
                        0
                      |) in
                    let r := M.alloc (| γ2_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (| "core::cmp::Ord", T, [], "cmp", [] |),
                        [ M.read (| l |); M.read (| r |) ]
                      |)
                    |)));
                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 γ0_0 := M.read (| γ0_0 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "core::option::Option::Some",
                        0
                      |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let _ := M.is_struct_tuple (| γ0_1, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::cmp::Ordering::Greater" [] |)));
                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 γ0_0 := M.read (| γ0_0 |) in
                    let _ := M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_1,
                        "core::option::Option::Some",
                        0
                      |) in
                    M.alloc (| Value.StructTuple "core::cmp::Ordering::Less" [] |)));
                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 γ0_0 := M.read (| γ0_0 |) in
                    let _ := M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let _ := M.is_struct_tuple (| γ0_1, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::cmp::Ordering::Equal" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::cmp::Ord"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method (cmp T)) ].
  End Impl_core_cmp_Ord_where_core_cmp_Ord_T_for_core_option_Option_T.
  
  (* StructRecord
    {
      name := "Item";
      const_params := [];
      ty_params := [ "A" ];
      fields := [ ("opt", Ty.apply (Ty.path "core::option::Option") [] [ A ]) ];
    } *)
  
  Module Impl_core_clone_Clone_where_core_clone_Clone_A_for_core_option_Item_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Item") [] [ A ].
    
    (* Clone *)
    Definition clone (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::option::Item"
            [
              ("opt",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply (Ty.path "core::option::Option") [] [ A ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::option::Item",
                      "opt"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone A)) ].
  End Impl_core_clone_Clone_where_core_clone_Clone_A_for_core_option_Item_A.
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_A_for_core_option_Item_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Item") [] [ A ].
    
    (* Debug *)
    Definition fmt (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "Item" |);
              M.read (| Value.String "opt" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::option::Item",
                  "opt"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt A)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_A_for_core_option_Item_A.
  
  Module Impl_core_iter_traits_iterator_Iterator_for_core_option_Item_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Item") [] [ A ].
    
    (*     type Item = A; *)
    Definition _Item (A : Ty.t) : Ty.t := A.
    
    (*
        fn next(&mut self) -> Option<A> {
            self.opt.take()
        }
    *)
    Definition next (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ A ],
              "take",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::option::Item",
                "opt"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn size_hint(&self) -> (usize, Option<usize>) {
            let len = self.len();
            (len, Some(len))
        }
    *)
    Definition size_hint (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ len :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::exact_size::ExactSizeIterator",
                    Ty.apply (Ty.path "core::option::Item") [] [ A ],
                    [],
                    "len",
                    []
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            M.alloc (|
              Value.Tuple
                [
                  M.read (| len |);
                  Value.StructTuple "core::option::Option::Some" [ M.read (| len |) ]
                ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::iterator::Iterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item A));
          ("next", InstanceField.Method (next A));
          ("size_hint", InstanceField.Method (size_hint A))
        ].
  End Impl_core_iter_traits_iterator_Iterator_for_core_option_Item_A.
  
  Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_option_Item_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Item") [] [ A ].
    
    (*
        fn next_back(&mut self) -> Option<A> {
            self.opt.take()
        }
    *)
    Definition next_back (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ A ],
              "take",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::option::Item",
                "opt"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::double_ended::DoubleEndedIterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("next_back", InstanceField.Method (next_back A)) ].
  End Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_option_Item_A.
  
  Module Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_option_Item_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Item") [] [ A ].
    
    (*
        fn len(&self) -> usize {
            self.opt.len()
        }
    *)
    Definition len (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ A ],
              "len",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::option::Item",
                "opt"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::exact_size::ExactSizeIterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("len", InstanceField.Method (len A)) ].
  End Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_option_Item_A.
  
  Module Impl_core_iter_traits_marker_FusedIterator_for_core_option_Item_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Item") [] [ A ].
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::marker::FusedIterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_FusedIterator_for_core_option_Item_A.
  
  Module Impl_core_iter_traits_marker_TrustedLen_for_core_option_Item_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Item") [] [ A ].
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::marker::TrustedLen"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_TrustedLen_for_core_option_Item_A.
  
  (* StructRecord
    {
      name := "Iter";
      const_params := [];
      ty_params := [ "A" ];
      fields :=
        [ ("inner", Ty.apply (Ty.path "core::option::Item") [] [ Ty.apply (Ty.path "&") [] [ A ] ])
        ];
    } *)
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_A_for_core_option_Iter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Iter") [] [ A ].
    
    (* Debug *)
    Definition fmt (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "Iter" |);
              M.read (| Value.String "inner" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::option::Iter",
                  "inner"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt A)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_A_for_core_option_Iter_A.
  
  Module Impl_core_iter_traits_iterator_Iterator_for_core_option_Iter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Iter") [] [ A ].
    
    (*     type Item = &'a A; *)
    Definition _Item (A : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ A ].
    
    (*
        fn next(&mut self) -> Option<&'a A> {
            self.inner.next()
        }
    *)
    Definition next (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::iterator::Iterator",
              Ty.apply (Ty.path "core::option::Item") [] [ Ty.apply (Ty.path "&") [] [ A ] ],
              [],
              "next",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::option::Iter",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn size_hint(&self) -> (usize, Option<usize>) {
            self.inner.size_hint()
        }
    *)
    Definition size_hint (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::iterator::Iterator",
              Ty.apply (Ty.path "core::option::Item") [] [ Ty.apply (Ty.path "&") [] [ A ] ],
              [],
              "size_hint",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::option::Iter",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::iterator::Iterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item A));
          ("next", InstanceField.Method (next A));
          ("size_hint", InstanceField.Method (size_hint A))
        ].
  End Impl_core_iter_traits_iterator_Iterator_for_core_option_Iter_A.
  
  Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_option_Iter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Iter") [] [ A ].
    
    (*
        fn next_back(&mut self) -> Option<&'a A> {
            self.inner.next_back()
        }
    *)
    Definition next_back (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::double_ended::DoubleEndedIterator",
              Ty.apply (Ty.path "core::option::Item") [] [ Ty.apply (Ty.path "&") [] [ A ] ],
              [],
              "next_back",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::option::Iter",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::double_ended::DoubleEndedIterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("next_back", InstanceField.Method (next_back A)) ].
  End Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_option_Iter_A.
  
  Module Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_option_Iter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Iter") [] [ A ].
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::exact_size::ExactSizeIterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_option_Iter_A.
  
  Module Impl_core_iter_traits_marker_FusedIterator_for_core_option_Iter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Iter") [] [ A ].
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::marker::FusedIterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_FusedIterator_for_core_option_Iter_A.
  
  Module Impl_core_iter_traits_marker_TrustedLen_for_core_option_Iter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Iter") [] [ A ].
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::marker::TrustedLen"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_TrustedLen_for_core_option_Iter_A.
  
  Module Impl_core_clone_Clone_for_core_option_Iter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Iter") [] [ A ].
    
    (*
        fn clone(&self) -> Self {
            Iter { inner: self.inner.clone() }
        }
    *)
    Definition clone (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::option::Iter"
            [
              ("inner",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply (Ty.path "core::option::Item") [] [ Ty.apply (Ty.path "&") [] [ A ] ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::option::Iter",
                      "inner"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone A)) ].
  End Impl_core_clone_Clone_for_core_option_Iter_A.
  
  (* StructRecord
    {
      name := "IterMut";
      const_params := [];
      ty_params := [ "A" ];
      fields :=
        [
          ("inner",
            Ty.apply (Ty.path "core::option::Item") [] [ Ty.apply (Ty.path "&mut") [] [ A ] ])
        ];
    } *)
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_A_for_core_option_IterMut_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IterMut") [] [ A ].
    
    (* Debug *)
    Definition fmt (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "IterMut" |);
              M.read (| Value.String "inner" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::option::IterMut",
                  "inner"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt A)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_A_for_core_option_IterMut_A.
  
  Module Impl_core_iter_traits_iterator_Iterator_for_core_option_IterMut_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IterMut") [] [ A ].
    
    (*     type Item = &'a mut A; *)
    Definition _Item (A : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ A ].
    
    (*
        fn next(&mut self) -> Option<&'a mut A> {
            self.inner.next()
        }
    *)
    Definition next (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::iterator::Iterator",
              Ty.apply (Ty.path "core::option::Item") [] [ Ty.apply (Ty.path "&mut") [] [ A ] ],
              [],
              "next",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::option::IterMut",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn size_hint(&self) -> (usize, Option<usize>) {
            self.inner.size_hint()
        }
    *)
    Definition size_hint (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::iterator::Iterator",
              Ty.apply (Ty.path "core::option::Item") [] [ Ty.apply (Ty.path "&mut") [] [ A ] ],
              [],
              "size_hint",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::option::IterMut",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::iterator::Iterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item A));
          ("next", InstanceField.Method (next A));
          ("size_hint", InstanceField.Method (size_hint A))
        ].
  End Impl_core_iter_traits_iterator_Iterator_for_core_option_IterMut_A.
  
  Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_option_IterMut_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IterMut") [] [ A ].
    
    (*
        fn next_back(&mut self) -> Option<&'a mut A> {
            self.inner.next_back()
        }
    *)
    Definition next_back (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::double_ended::DoubleEndedIterator",
              Ty.apply (Ty.path "core::option::Item") [] [ Ty.apply (Ty.path "&mut") [] [ A ] ],
              [],
              "next_back",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::option::IterMut",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::double_ended::DoubleEndedIterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("next_back", InstanceField.Method (next_back A)) ].
  End Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_option_IterMut_A.
  
  Module Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_option_IterMut_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IterMut") [] [ A ].
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::exact_size::ExactSizeIterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_option_IterMut_A.
  
  Module Impl_core_iter_traits_marker_FusedIterator_for_core_option_IterMut_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IterMut") [] [ A ].
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::marker::FusedIterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_FusedIterator_for_core_option_IterMut_A.
  
  Module Impl_core_iter_traits_marker_TrustedLen_for_core_option_IterMut_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IterMut") [] [ A ].
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::marker::TrustedLen"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_TrustedLen_for_core_option_IterMut_A.
  
  (* StructRecord
    {
      name := "IntoIter";
      const_params := [];
      ty_params := [ "A" ];
      fields := [ ("inner", Ty.apply (Ty.path "core::option::Item") [] [ A ]) ];
    } *)
  
  Module Impl_core_clone_Clone_where_core_clone_Clone_A_for_core_option_IntoIter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IntoIter") [] [ A ].
    
    (* Clone *)
    Definition clone (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.StructRecord
            "core::option::IntoIter"
            [
              ("inner",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply (Ty.path "core::option::Item") [] [ A ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "core::option::IntoIter",
                      "inner"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::clone::Clone"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method (clone A)) ].
  End Impl_core_clone_Clone_where_core_clone_Clone_A_for_core_option_IntoIter_A.
  
  Module Impl_core_fmt_Debug_where_core_fmt_Debug_A_for_core_option_IntoIter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IntoIter") [] [ A ].
    
    (* Debug *)
    Definition fmt (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "IntoIter" |);
              M.read (| Value.String "inner" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "core::option::IntoIter",
                  "inner"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt A)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Debug_A_for_core_option_IntoIter_A.
  
  Module Impl_core_iter_traits_iterator_Iterator_for_core_option_IntoIter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IntoIter") [] [ A ].
    
    (*     type Item = A; *)
    Definition _Item (A : Ty.t) : Ty.t := A.
    
    (*
        fn next(&mut self) -> Option<A> {
            self.inner.next()
        }
    *)
    Definition next (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::iterator::Iterator",
              Ty.apply (Ty.path "core::option::Item") [] [ A ],
              [],
              "next",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::option::IntoIter",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn size_hint(&self) -> (usize, Option<usize>) {
            self.inner.size_hint()
        }
    *)
    Definition size_hint (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::iterator::Iterator",
              Ty.apply (Ty.path "core::option::Item") [] [ A ],
              [],
              "size_hint",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::option::IntoIter",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::iterator::Iterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Item", InstanceField.Ty (_Item A));
          ("next", InstanceField.Method (next A));
          ("size_hint", InstanceField.Method (size_hint A))
        ].
  End Impl_core_iter_traits_iterator_Iterator_for_core_option_IntoIter_A.
  
  Module Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_option_IntoIter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IntoIter") [] [ A ].
    
    (*
        fn next_back(&mut self) -> Option<A> {
            self.inner.next_back()
        }
    *)
    Definition next_back (A : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::double_ended::DoubleEndedIterator",
              Ty.apply (Ty.path "core::option::Item") [] [ A ],
              [],
              "next_back",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "core::option::IntoIter",
                "inner"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::double_ended::DoubleEndedIterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("next_back", InstanceField.Method (next_back A)) ].
  End Impl_core_iter_traits_double_ended_DoubleEndedIterator_for_core_option_IntoIter_A.
  
  Module Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_option_IntoIter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IntoIter") [] [ A ].
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::exact_size::ExactSizeIterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_exact_size_ExactSizeIterator_for_core_option_IntoIter_A.
  
  Module Impl_core_iter_traits_marker_FusedIterator_for_core_option_IntoIter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IntoIter") [] [ A ].
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::marker::FusedIterator"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_FusedIterator_for_core_option_IntoIter_A.
  
  Module Impl_core_iter_traits_marker_TrustedLen_for_core_option_IntoIter_A.
    Definition Self (A : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::IntoIter") [] [ A ].
    
    Axiom Implements :
      forall (A : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::marker::TrustedLen"
        (Self A)
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_iter_traits_marker_TrustedLen_for_core_option_IntoIter_A.
  
  Module Impl_core_iter_traits_collect_FromIterator_where_core_iter_traits_collect_FromIterator_V_A_core_option_Option_A_for_core_option_Option_V.
    Definition Self (A V : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ V ].
    
    (*
        fn from_iter<I: IntoIterator<Item = Option<A>>>(iter: I) -> Option<V> {
            // FIXME(#11084): This could be replaced with Iterator::scan when this
            // performance bug is closed.
    
            iter::try_process(iter.into_iter(), |i| i.collect())
        }
    *)
    Definition from_iter (A V : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self A V in
      match ε, τ, α with
      | [], [ _ as I ], [ iter ] =>
        ltac:(M.monadic
          (let iter := M.alloc (| iter |) in
          M.call_closure (|
            M.get_function (|
              "core::iter::adapters::try_process",
              [
                Ty.associated;
                A;
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.path "core::convert::Infallible" ];
                Ty.function
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "core::iter::adapters::GenericShunt")
                          []
                          [
                            Ty.associated;
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "core::convert::Infallible" ]
                          ]
                      ]
                  ]
                  V;
                V
              ]
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::collect::IntoIterator",
                  I,
                  [],
                  "into_iter",
                  []
                |),
                [ M.read (| iter |) ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let i := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::iterator::Iterator",
                                    Ty.apply
                                      (Ty.path "core::iter::adapters::GenericShunt")
                                      []
                                      [
                                        Ty.associated;
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [ Ty.path "core::convert::Infallible" ]
                                      ],
                                    [],
                                    "collect",
                                    [ V ]
                                  |),
                                  [ M.read (| i |) ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (A V : Ty.t),
      M.IsTraitInstance
        "core::iter::traits::collect::FromIterator"
        (Self A V)
        (* Trait polymorphic types *) [ (* A *) Ty.apply (Ty.path "core::option::Option") [] [ A ] ]
        (* Instance *) [ ("from_iter", InstanceField.Method (from_iter A V)) ].
  End Impl_core_iter_traits_collect_FromIterator_where_core_iter_traits_collect_FromIterator_V_A_core_option_Option_A_for_core_option_Option_V.
  
  Module Impl_core_ops_try_trait_Try_for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    (*     type Output = T; *)
    Definition _Output (T : Ty.t) : Ty.t := T.
    
    (*     type Residual = Option<convert::Infallible>; *)
    Definition _Residual (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "core::convert::Infallible" ].
    
    (*
        fn from_output(output: Self::Output) -> Self {
            Some(output)
        }
    *)
    Definition from_output (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ output ] =>
        ltac:(M.monadic
          (let output := M.alloc (| output |) in
          Value.StructTuple "core::option::Option::Some" [ M.read (| output |) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn branch(self) -> ControlFlow<Self::Residual, Self::Output> {
            match self {
                Some(v) => ControlFlow::Continue(v),
                None => ControlFlow::Break(None),
            }
        }
    *)
    Definition branch (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let v := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::ops::control_flow::ControlFlow::Continue"
                        [ M.read (| v |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::ops::control_flow::ControlFlow::Break"
                        [ Value.StructTuple "core::option::Option::None" [] ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::try_trait::Try"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Output", InstanceField.Ty (_Output T));
          ("Residual", InstanceField.Ty (_Residual T));
          ("from_output", InstanceField.Method (from_output T));
          ("branch", InstanceField.Method (branch T))
        ].
  End Impl_core_ops_try_trait_Try_for_core_option_Option_T.
  
  Module Impl_core_ops_try_trait_FromResidual_core_option_Option_core_convert_Infallible_for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    (*
        fn from_residual(residual: Option<convert::Infallible>) -> Self {
            match residual {
                None => None,
            }
        }
    *)
    Definition from_residual (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ residual ] =>
        ltac:(M.monadic
          (let residual := M.alloc (| residual |) in
          M.read (|
            M.match_operator (|
              residual,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::try_trait::FromResidual"
        (Self T)
        (* Trait polymorphic types *)
        [
          (* R *)
          Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "core::convert::Infallible" ]
        ]
        (* Instance *) [ ("from_residual", InstanceField.Method (from_residual T)) ].
  End Impl_core_ops_try_trait_FromResidual_core_option_Option_core_convert_Infallible_for_core_option_Option_T.
  
  Module Impl_core_ops_try_trait_FromResidual_core_ops_try_trait_Yeet_Tuple__for_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    (*
        fn from_residual(ops::Yeet(()): ops::Yeet<()>) -> Self {
            None
        }
    *)
    Definition from_residual (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ β0 ] =>
        ltac:(M.monadic
          (let β0 := M.alloc (| β0 |) in
          M.match_operator (|
            β0,
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::ops::try_trait::Yeet", 0 |) in
                  Value.StructTuple "core::option::Option::None" []))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::try_trait::FromResidual"
        (Self T)
        (* Trait polymorphic types *)
        [ (* R *) Ty.apply (Ty.path "core::ops::try_trait::Yeet") [] [ Ty.tuple [] ] ]
        (* Instance *) [ ("from_residual", InstanceField.Method (from_residual T)) ].
  End Impl_core_ops_try_trait_FromResidual_core_ops_try_trait_Yeet_Tuple__for_core_option_Option_T.
  
  Module Impl_core_ops_try_trait_Residual_T_for_core_option_Option_core_convert_Infallible.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "core::convert::Infallible" ].
    
    (*     type TryType = Option<T>; *)
    Definition _TryType (T : Ty.t) : Ty.t := Ty.apply (Ty.path "core::option::Option") [] [ T ].
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::ops::try_trait::Residual"
        (Self T)
        (* Trait polymorphic types *) [ (* O *) T ]
        (* Instance *) [ ("TryType", InstanceField.Ty (_TryType T)) ].
  End Impl_core_ops_try_trait_Residual_T_for_core_option_Option_core_convert_Infallible.
  
  Module Impl_core_option_Option_core_option_Option_T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply
        (Ty.path "core::option::Option")
        []
        [ Ty.apply (Ty.path "core::option::Option") [] [ T ] ].
    
    (*
        pub const fn flatten(self) -> Option<T> {
            // FIXME(const-hack): could be written with `and_then`
            match self {
                Some(inner) => inner,
                None => None,
            }
        }
    *)
    Definition flatten (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let inner := M.copy (| γ0_0 |) in
                    inner));
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_flatten :
      forall (T : Ty.t),
      M.IsAssociatedFunction (Self T) "flatten" (flatten T).
  End Impl_core_option_Option_core_option_Option_T.
End option.
