hs-to-coq
hs-to-coq copied to clipboard
antalsz
Convert Haskell source code to Coq source code
The add edit only adds stuff after the midamble. Sometimes we want to add before that.
In GHC, when we remove type information it would be useful to just eliminate the part of the data structure entirely instead of mapping it to unit. This requires figuring...
It might be nice to impose "default order" constraints, such as * For all types `T`, put `Semigroup` before `mappend` (i.e., `Semigroup__T` before `Monoid__T_mappend`) * For all types `T`, put...
Coq has an easier time doing termination proofs when we pull out fixpoint arguments that don't change. For instance, in GHC's `compiler/utils/Util.hs`, we find the function ```haskell -- Reformatted all2...
Right now, if we define a class `C` manually, we can never translate instances of `C` because the class info lookup fails. We need a way to provide the `h2ci`...
It seems like there's a lot of code lying around that isn't being run anymore. Someone who has some spare time should go through and delete it.
@sweirich in [a comment] on commit 4cd6596, about `unaxiomatize definition`: > How about something a little more general, so that we can have "skip everything except for this" too. >...
Consider the following painfully contrived Haskell code: ```haskell module BadMut where data Nat = Z | S Nat sink :: Nat -> a -> a sink Z x = x...
As we saw in #100 (preserving record names), our story for tracking `Default` instances isn't great and needs some manual skipping. As I understand it, #100 introduces too many `Default`...