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

Module inspector.
  Module noop.
    (* StructTuple
      {
        name := "NoOpInspector";
        const_params := [];
        ty_params := [];
        fields := [];
      } *)
    
    Module Impl_core_clone_Clone_for_revm_inspector_noop_NoOpInspector.
      Definition Self : Ty.t := Ty.path "revm::inspector::noop::NoOpInspector".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_revm_inspector_noop_NoOpInspector.
    
    Module Impl_core_marker_Copy_for_revm_inspector_noop_NoOpInspector.
      Definition Self : Ty.t := Ty.path "revm::inspector::noop::NoOpInspector".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_revm_inspector_noop_NoOpInspector.
    
    Module Impl_core_fmt_Debug_for_revm_inspector_noop_NoOpInspector.
      Definition Self : Ty.t := Ty.path "revm::inspector::noop::NoOpInspector".
      
      (* 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 "NoOpInspector" |) ]
            |)))
        | _, _, _ => 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_revm_inspector_noop_NoOpInspector.
    
    Module Impl_core_default_Default_for_revm_inspector_noop_NoOpInspector.
      Definition Self : Ty.t := Ty.path "revm::inspector::noop::NoOpInspector".
      
      (* Default *)
      Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic (Value.StructTuple "revm::inspector::noop::NoOpInspector" []))
        | _, _, _ => 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_revm_inspector_noop_NoOpInspector.
    
    Module Impl_core_marker_StructuralPartialEq_for_revm_inspector_noop_NoOpInspector.
      Definition Self : Ty.t := Ty.path "revm::inspector::noop::NoOpInspector".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_revm_inspector_noop_NoOpInspector.
    
    Module Impl_core_cmp_PartialEq_for_revm_inspector_noop_NoOpInspector.
      Definition Self : Ty.t := Ty.path "revm::inspector::noop::NoOpInspector".
      
      (* 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_revm_inspector_noop_NoOpInspector.
    
    Module Impl_core_cmp_Eq_for_revm_inspector_noop_NoOpInspector.
      Definition Self : Ty.t := Ty.path "revm::inspector::noop::NoOpInspector".
      
      (* 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_revm_inspector_noop_NoOpInspector.
    
    Module Impl_core_cmp_PartialOrd_for_revm_inspector_noop_NoOpInspector.
      Definition Self : Ty.t := Ty.path "revm::inspector::noop::NoOpInspector".
      
      (* 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_revm_inspector_noop_NoOpInspector.
    
    Module Impl_core_cmp_Ord_for_revm_inspector_noop_NoOpInspector.
      Definition Self : Ty.t := Ty.path "revm::inspector::noop::NoOpInspector".
      
      (* 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_revm_inspector_noop_NoOpInspector.
    
    Module Impl_core_hash_Hash_for_revm_inspector_noop_NoOpInspector.
      Definition Self : Ty.t := Ty.path "revm::inspector::noop::NoOpInspector".
      
      (* 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_revm_inspector_noop_NoOpInspector.
    
    Module Impl_revm_inspector_Inspector_where_revm_primitives_db_Database_DB_DB_for_revm_inspector_noop_NoOpInspector.
      Definition Self (DB : Ty.t) : Ty.t := Ty.path "revm::inspector::noop::NoOpInspector".
      
      Axiom Implements :
        forall (DB : Ty.t),
        M.IsTraitInstance
          "revm::inspector::Inspector"
          (Self DB)
          (* Trait polymorphic types *) [ (* DB *) DB ]
          (* Instance *) [].
    End Impl_revm_inspector_Inspector_where_revm_primitives_db_Database_DB_DB_for_revm_inspector_noop_NoOpInspector.
  End noop.
End inspector.
