agda2hs

agda2hs copied to clipboard

Integrate agda2hs with cabal

5

jespercockx

to complement All

jakobn-ai

[ fix #302 ] Move _/=_ function out of the Eq record

1

jespercockx

maps and set

3

Add support for maps and sets

jmchapman

_/=_ generates incorrect `iEq…`

1

```agda not0 : Int → Bool not0 n = n /= 0 {-# COMPILE AGDA2HS not0 #-} ``` generates ```haskell import qualified Prelude ((/=)) not0 :: Int -> Bool not0...

jakobn-ai

Adding mechanism for skipping up-to-date files

5

Now, agda2hs skips every Agda file for which the corresponding Haskell file is newer _than the `.agdai` file_. For this, I had to replace the `moduleFileName` function from Render.hs and...

viktorcsimma

Guards

9

Writing functions with pattern guards is idiomatic in Haskell, but it is currently not supported by agda2hs. I can think of two ways this could be supported: 1. We translate...

jespercockx

Bug reported by @liesnikov. ```agda private variable @0 a : Set Ap : (p : @0 a → Set) → @0 a → Set Ap p x = p x...

flupe

This is the remaining issue with parametrized modules after the merging of https://github.com/agda/agda2hs/pull/307: ```agda record Class (a : Set) : Set where field foo : a → a open Class...

jespercockx

When defining an unboxed record, one gets to define new instances for type classes on the Agda side. Those instances never get compiled, and code that uses instances over boxed...

flupe