Skip to content
This repository has been archived by the owner on Nov 17, 2020. It is now read-only.

Skip types from a skipped module #166

Open
Lysxia opened this issue Oct 17, 2020 · 0 comments
Open

Skip types from a skipped module #166

Lysxia opened this issue Oct 17, 2020 · 0 comments

Comments

@Lysxia
Copy link
Contributor

Lysxia commented Oct 17, 2020

Trying to translate base-4.14, some modules (like Data.Foldable) mention types from skipped modules (like GHC.Generics.UWord), which causes the translation to fail. In particular, in this case the type is mentioned in an instance so it can't be worked around by skipping the value instead. Actually you can skip an instance, since they are referred to by their Coq name!

A naive solution is to skip uses of types from skipped modules, but the actual situation is a little trickier because those types can also be renamed, in which case they shouldn't be skipped.

This is related to #35 which is about skipping uses of individual types. And #39 would be fixed by the presently proposed feature.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant