agda/agda2hs

Issues

• nix binary ignores interface files

  #321 opened 3 months ago by stites
  5

• Can't build agda2hs with recent GHC version(s)

  #378 opened 2 months ago by abailly
  6

• Allow `existing-class` for postulated type classes

  #373 opened 3 months ago by flupe
  0

• Compiling declared but not-yet-defined datatype silently generates no code

  #346 opened 5 months ago by jespercockx
  0

• Imports of modules that have current module name as prefix are dropped silently

  #338 opened 6 months ago by jespercockx
  0

• No import generated for `fromMaybe`

  #377 opened 3 months ago by jespercockx
  0

• Support building with GHC 9.10 (base-4.20)

  #347 opened 3 months ago by cho-m
  1

• Error: pattern matching lambdas must take a single argument

  #340 opened 5 months ago by jespercockx
  0

• Erroneous assumption about lambda precedence in generated code

  #317 opened 6 months ago by bwbush
  1

• Release agda2hs 1.3

  #366 opened 3 months ago by jespercockx
  26

• Macro generates variable with out-of-scope name

  #344 opened 5 months ago by jespercockx
  0

• agda2hs inlines function with explicit `forall` but not without

  #376 opened 3 months ago by jespercockx
  1

• Add agda2hs library to data-files + add command to print location of the library

  #370 opened 3 months ago by jespercockx
  0

• Rename `Rezz` to `Singleton`

  #371 opened 3 months ago by flupe
  0

• Better error when compiling level definitions

  #355 opened 3 months ago by omelkonian
  1

• Agda does not accept equational reasoning with `if_then_else` and erased invariants

  #361 opened 3 months ago by HeinrichApfelmus
  7

• Support using instances from applied modules in canonicity check

  #308 opened 3 months ago by jespercockx
  1

• Wrong argument is dropped for projection-like function in parametrized module

  #359 opened 3 months ago by jespercockx
  0

• Parse errors on deriving clauses a class itself causes a crash

  #351 opened 3 months ago by anka-213
  0

• Calling between functions in (multiple) anonymous modules causes arguments to disappear

  #353 opened 3 months ago by anka-213
  5

• Levels should not always be erased

  #357 opened 3 months ago by omelkonian
  5

• Internal error using DefaultMonoid

  #301 opened 9 months ago by naucke
  1

• Usage of Sigma adds an incorrect import and forgets brackets

  #310 opened 8 months ago by sarajuhosova
  0

• Support generating RankN haskell types (using forall)

  #352 opened 3 months ago by anka-213
  1

• Update Agda base to 2.7.0

  #349 opened 3 months ago by jespercockx
  0

• Incorrect transpilation of polymorphic `where` clauses

  #362 opened 3 months ago by HeinrichApfelmus
  12

• Support `hiding` things from the prelude

  #356 opened 4 months ago by omelkonian
  0

• Typeclass instances not imported.

  #324 opened 8 months ago by bwbush
  0

• Address inconsistent style of typeclass laws

  #336 opened 6 months ago by omelkonian
  0

• `agda2hs` fails unless `agda` or `agda2hs` is run first

  #322 opened 8 months ago by bwbush
  2

• New `≡⟨_⟨` syntax for `≡˘⟨_⟩`?

  #334 opened 7 months ago by pmbittner
  0

• Compile multiple arguments pattern lambda to multi-way lambda expressions

  #335 opened 6 months ago by flupe
  0

• Incorrect compilation of type synonyms

  #309 opened 7 months ago by flupe
  1

• Dot patterns in arguments corresponding to module parameters should not be allowed

  #306 opened 9 months ago by jespercockx
  0

• Postulates are not exported

  #323 opened 7 months ago by bwbush
  5

• Newtype constructor erroneously removed

  #320 opened 8 months ago by bwbush
  2

• Unary operators

  #319 opened 7 months ago by bwbush
  3

• _/=_ generates incorrect `iEq…`

  #302 opened 7 months ago by naucke
  1

• Definition of `Functor` is inconsistent with `base-4.18.1.0` etc.

  #318 opened 8 months ago by bwbush
  1

• Better support for wrapping Haskell modules via `postulate`

  #316 opened 8 months ago by HeinrichApfelmus
  2

• Typeclass functions in parametrized modules do not work

  #305 opened 9 months ago by jespercockx
  0

• Docs: add `syntax` trick to use Unicode instead of Haskell-compatible ASCII identifiers

  #293 opened 10 months ago by omelkonian
  1

• Add support for older GHC versions 8.6.5 and 9.02

  #281 opened 10 months ago by omelkonian
  0

• Support constructors in rewrite rules

  #283 opened 10 months ago by celsobonutti
  2

• Consider using `ghc-source-gen`

  #274 opened a year ago by flupe
  0

• Bad compilation of integer literal to `int64 (Prelude.primWord64FromNat ...)`

  #286 opened 10 months ago by jespercockx
  0

• Cannot set RTS flags

  #278 opened 10 months ago by omelkonian
  0

• `snd $` compiles incorrectly

  #273 opened a year ago by HeinrichApfelmus
  8

• Add support for associated type families

  #288 opened 10 months ago by jespercockx
  1

• Agda internally eta-reduces when it shouldn't

  #275 opened a year ago by omelkonian
  0