You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Aeneas translates trait methods that have a default body because in the future we may want to refer to them. These methods are named Trait::method, which in Lean causes a name clash with the method field of Trait: both would be named Trait.method. To avoid this clash, in #437 we rename these methods to Trait::default::method.
This however could still cause clashes with a method named default. We should find a naming scheme that is unlikely to clash with other names.
The text was updated successfully, but these errors were encountered:
Aeneas translates trait methods that have a default body because in the future we may want to refer to them. These methods are named
Trait::method
, which in Lean causes a name clash with themethod
field ofTrait
: both would be namedTrait.method
. To avoid this clash, in #437 we rename these methods toTrait::default::method
.This however could still cause clashes with a method named
default
. We should find a naming scheme that is unlikely to clash with other names.The text was updated successfully, but these errors were encountered: