hs-to-coq
hs-to-coq copied to clipboard
antalsz
Convert Haskell source code to Coq source code
After the ICFP talk, “Robbert” pointed out that [Jacques-Henri Jourdan's PhD thesis](https://jhjourdan.mketjh.fr/thesis_jhjourdan.pdf) in Section 9.1 describes a problem with out encoding of `ptrEq`, and how to fix it. We could...
The following way of declaring a monad instance is quite common in Haskell: ```haskell instance Monad Hp where return = returnHp m >>= f = bindHp m f instance Applicative...
In `examples/containers/module-edits/Data/IntSet/Internal/edits`, there is the following line right at the top: `rename type GHC.Types.Int = Coq.Numbers.BinNums.N` Shouldn't that be `rename type GHC.Types.Int = Coq.Numbers.BinNums.Z`instead?
In a file that I'm generating with hs-to-coq, there appears the line `Require Deriving.`. I don't know why this line is generated (I suspect it is related to the `DeriveGeneric`...
Just added a TON of order directives to make sure that Uniquable Var comes before everything that depends on it. Is there anything to be done about this? We are...
Right now axiomatize module has the potential to introduce inconsistent axioms. We could fix this by using default instead. I.e. instead of generating ``` Axiom mkFoo : Int -> Char...
When I extract Coq code generated by hs-to-coq back to Haskell using Coq's Extraction command, I get a lot of warnings like this: ``` Warning: The identifier arg_0__ contains __...
We can't say: ```(x,y) = (True,False)``` This occurs in `PrelNames`, but low priority. We probably want to manually axiomatize this module anyways. Just making the issue to mark this as...
See `StrictPair` in the test cases. Can be worked-around by renaming data constructors to something that is not a symbol.