agda2hs
agda2hs copied to clipboard
agda
Compiling Agda code to readable Haskell
Need to go through all files and decide what's public, what's private, etc..
Currently the test infrastructure for agda2hs is stupid: for each test we need to add an import to AllTests.hs or else the test is not actually run. Instead we could...
When using a Haskell function that has been verified using Agda2Hs, it would be nice if we could also use the verified properties of that function as Liquid Haskell refinements....
It would be nice to add support for equality constraints in generated Haskell code. A way to represent this on the Agda side would be to use instance arguments with...
It would be interesting to be able to postulate properties using `IsTrue` that are translated to QuickCheck tests on the Haskell side. This would provide a more gradual way of...
(Context: #29) Agda doesn't have any builtin 32-bit numerical types, so it's not clear how to best support 32-bit platforms (if at all). Some options (in order of less work...
Lifting the upper bound of `base` does allow build to succeed: https://github.com/agda/agda2hs/blob/7753783a316de2db07da627f47058ed83bbc9876/agda2hs.cabal#L63 --- Opened this as working on updating to GHC 9.10.1 in Homebrew (https://github.com/Homebrew/homebrew-core/pull/178590) and noticed the Homebrew `agda`...
Minimal example: ```agda data D : Set {-# COMPILE AGDA2HS D #-} data D where C : D ``` This generates an empty Haskell file. It should either raise an...