```coq
Definition Self : Ty.t := Ty.path "core::fmt::Error".
(* ... *)
Axiom Implements :
M.IsTraitInstance
"core::cmp::PartialEq"
(* Trait polymorphic consts *) []
(* Trait polymorphic types *) []
Self
(* Instance *) [ ("eq", InstanceField.Method eq) ].
```
Definition Self : Ty.t := Ty.path "core::fmt::Error".
(* ... *)
Axiom Implements :
M.IsTraitInstance
"core::cmp::PartialEq"
(* Trait polymorphic consts *) []
(* Trait polymorphic types *) []
Self
(* Instance *) [ ("eq", InstanceField.Method eq) ].
```
Comments
After our fix, we correctly get:
Axiom Implements :
M.IsTraitInstance
"core::cmp::PartialEq"
(* Trait polymorphic consts *) []
(* Trait polymorphic types *) [ Ty.path "core::fmt::Error" ]
Self
(* Instance *) [ ("eq", InstanceField.Method eq) ].
```
We also added support for `const` parameters for traits that are rarely used but still occurred in one of the codes we looked at.
Fortunately, as we are verifying more code, we make `coq-of-rust` more reliable and add more examples in our CI!