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
When possible, the special treatment for the fstar backend implemented in #1075 (see the discussion in the PR for the reason) should be removed. It is a hack to allow type class methods to be accessible in the original modules and not only in the bundle. But it is specific to the use we have for type classes for the translation of traits.
The text was updated successfully, but these errors were encountered:
Fixing #412 will indeed fix this issue as well, thanks Franziskus!
The special treatment Maxime talks about is related to the fact F* creates a top level function per type class method in the module the type class is defined in. So this will indeed go away as soon we stop replying on F* typeclasses.
When possible, the special treatment for the fstar backend implemented in #1075 (see the discussion in the PR for the reason) should be removed. It is a hack to allow type class methods to be accessible in the original modules and not only in the bundle. But it is specific to the use we have for type classes for the translation of traits.
The text was updated successfully, but these errors were encountered: