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

Module collections.
  Module btree.
    Module set_val.
      (* StructTuple
        {
          name := "SetValZST";
          const_params := [];
          ty_params := [];
          fields := [];
        } *)
      
      Module Impl_core_fmt_Debug_for_alloc_collections_btree_set_val_SetValZST.
        Definition Self : Ty.t := Ty.path "alloc::collections::btree::set_val::SetValZST".
        
        (* Debug *)
        Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
                [ M.read (| f |); M.read (| Value.String "SetValZST" |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::fmt::Debug"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
      End Impl_core_fmt_Debug_for_alloc_collections_btree_set_val_SetValZST.
      
      Module Impl_core_cmp_Eq_for_alloc_collections_btree_set_val_SetValZST.
        Definition Self : Ty.t := Ty.path "alloc::collections::btree::set_val::SetValZST".
        
        (* Eq *)
        Definition assert_receiver_is_total_eq
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.Tuple []))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::cmp::Eq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
      End Impl_core_cmp_Eq_for_alloc_collections_btree_set_val_SetValZST.
      
      Module Impl_core_marker_StructuralPartialEq_for_alloc_collections_btree_set_val_SetValZST.
        Definition Self : Ty.t := Ty.path "alloc::collections::btree::set_val::SetValZST".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_alloc_collections_btree_set_val_SetValZST.
      
      Module Impl_core_cmp_PartialEq_for_alloc_collections_btree_set_val_SetValZST.
        Definition Self : Ty.t := Ty.path "alloc::collections::btree::set_val::SetValZST".
        
        (* PartialEq *)
        Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              Value.Bool true))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::cmp::PartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("eq", InstanceField.Method eq) ].
      End Impl_core_cmp_PartialEq_for_alloc_collections_btree_set_val_SetValZST.
      
      Module Impl_core_cmp_Ord_for_alloc_collections_btree_set_val_SetValZST.
        Definition Self : Ty.t := Ty.path "alloc::collections::btree::set_val::SetValZST".
        
        (* Ord *)
        Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              Value.StructTuple "core::cmp::Ordering::Equal" []))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::cmp::Ord"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
      End Impl_core_cmp_Ord_for_alloc_collections_btree_set_val_SetValZST.
      
      Module Impl_core_cmp_PartialOrd_for_alloc_collections_btree_set_val_SetValZST.
        Definition Self : Ty.t := Ty.path "alloc::collections::btree::set_val::SetValZST".
        
        (* PartialOrd *)
        Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              Value.StructTuple
                "core::option::Option::Some"
                [ Value.StructTuple "core::cmp::Ordering::Equal" [] ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::cmp::PartialOrd"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
      End Impl_core_cmp_PartialOrd_for_alloc_collections_btree_set_val_SetValZST.
      
      Module Impl_core_hash_Hash_for_alloc_collections_btree_set_val_SetValZST.
        Definition Self : Ty.t := Ty.path "alloc::collections::btree::set_val::SetValZST".
        
        (* Hash *)
        Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ __H ], [ self; state ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let state := M.alloc (| state |) in
              Value.Tuple []))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::hash::Hash"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("hash", InstanceField.Method hash) ].
      End Impl_core_hash_Hash_for_alloc_collections_btree_set_val_SetValZST.
      
      Module Impl_core_clone_Clone_for_alloc_collections_btree_set_val_SetValZST.
        Definition Self : Ty.t := Ty.path "alloc::collections::btree::set_val::SetValZST".
        
        (* Clone *)
        Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructTuple "alloc::collections::btree::set_val::SetValZST" []))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::clone::Clone"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method clone) ].
      End Impl_core_clone_Clone_for_alloc_collections_btree_set_val_SetValZST.
      
      Module Impl_core_default_Default_for_alloc_collections_btree_set_val_SetValZST.
        Definition Self : Ty.t := Ty.path "alloc::collections::btree::set_val::SetValZST".
        
        (* Default *)
        Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic (Value.StructTuple "alloc::collections::btree::set_val::SetValZST" []))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::default::Default"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method default) ].
      End Impl_core_default_Default_for_alloc_collections_btree_set_val_SetValZST.
      
      (* Trait *)
      (* Empty module 'IsSetVal' *)
      
      Module Impl_alloc_collections_btree_set_val_IsSetVal_for_V.
        Definition Self (V : Ty.t) : Ty.t := V.
        
        (*
            default fn is_set_val() -> bool {
                false
            }
        *)
        Definition is_set_val
            (V : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self V in
          match ε, τ, α with
          | [], [], [] => ltac:(M.monadic (Value.Bool false))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (V : Ty.t),
          M.IsTraitInstance
            "alloc::collections::btree::set_val::IsSetVal"
            (Self V)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("is_set_val", InstanceField.Method (is_set_val V)) ].
      End Impl_alloc_collections_btree_set_val_IsSetVal_for_V.
      
      Module Impl_alloc_collections_btree_set_val_IsSetVal_for_alloc_collections_btree_set_val_SetValZST.
        Definition Self : Ty.t := Ty.path "alloc::collections::btree::set_val::SetValZST".
        
        (*
            fn is_set_val() -> bool {
                true
            }
        *)
        Definition is_set_val (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [] => ltac:(M.monadic (Value.Bool true))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "alloc::collections::btree::set_val::IsSetVal"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("is_set_val", InstanceField.Method is_set_val) ].
      End Impl_alloc_collections_btree_set_val_IsSetVal_for_alloc_collections_btree_set_val_SetValZST.
    End set_val.
  End btree.
End collections.
