Issues

• iLawfulOrdDouble is refuted by NaN and gives a proof of ⊥

  buglibrary
  agda/agda2hs#488 · Filter by author Ode-to-a-Nightingale opened on Nov 11, 2026 · 1.5
  1

• prop-member-map in Haskell.Data.Set is false for non-injective functions and gives a proof of ⊥

  buglibrary
  agda/agda2hs#487 · Filter by author Ode-to-a-Nightingale opened on Nov 11, 2026 · 1.5
  1

• Skipping compilation for up-to-date files results in mis-compilation

  bug
  agda/agda2hs#486 · Filter by author wasabi315 opened on Nov 6, 2026
  2

• Compile reexport of individual items

  enhancement
  agda/agda2hs#484 · Filter by author wasabi315 opened on Nov 4, 2026
  

• Compile module reexport

  enhancement
  agda/agda2hs#483 · Filter by author wasabi315 opened on Nov 4, 2026 · 1.5
  

• Compare things with α-equivalence

  bug
  agda/agda2hs#479 · Filter by author wasabi315 opened on Oct 27, 2026

• Support type operators in rewrite rules

  enhancement
  agda/agda2hs#473 · Filter by author wasabi315 opened on Oct 22, 2026

• COMPILE to definitions from Haskell.* modules

  enhancement
  agda/agda2hs#472 · Filter by author wasabi315 opened on Oct 22, 2026

• Compile abstract datatype/record

  enhancement
  agda/agda2hs#471 · Filter by author wasabi315 opened on Oct 22, 2026

• Update Agda version to 2.9.0

  agda/agda2hs#469 · Filter by author jespercockx opened on Oct 22, 2026 · 1.5
  2

• haskell-src-exts currently on life support

  agda/agda2hs#468 · Filter by author jespercockx opened on Oct 22, 2026

• Instance-search instances get inlined

  enhancement
  agda/agda2hs#458 · Filter by author ggrandi opened on Jun 8, 2026
  2

• agda2hs cannot compile Traversable instances defined with traverse=_

  buglibrary
  agda/agda2hs#457 · Filter by author ggrandi opened on Jun 1, 2026 · 1.5
  1

• Internal error for postulate in where block

  bug
  agda/agda2hs#443 · Filter by author jespercockx opened on Nov 18, 2025 · 1.5
  

• Add support for TypeRep and Typeable

  enhancementlibrary
  agda/agda2hs#441 · Filter by author jespercockx opened on Nov 17, 2025
  1

• Error "case_of_ must be fully applied to a lambda term in "Generate test-suite HTML" CI action

  bughelp wanted
  agda/agda2hs#436 · Filter by author jespercockx opened on Oct 10, 2025
  1

  

• Add functions from Control.Monad to the prelude

  enhancementlibrary
  agda/agda2hs#434 · Filter by author jespercockx opened on Oct 7, 2025

• Add support for functions from System.Environment

  enhancementgood first issuelibrary
  agda/agda2hs#433 · Filter by author jespercockx opened on Oct 7, 2025
  

• Add support for Exception typeclass and throw/catch functions

  enhancementlibrary
  agda/agda2hs#432 · Filter by author jespercockx opened on Oct 7, 2025 · 1.5
  1

  

• The assert function should not be used in erased positions

  bug
  agda/agda2hs#428 · Filter by author jespercockx opened on Sep 11, 2025 · 1.5
  6

  

• Monad, Applicative, Functor: Add equations for default definitions and superclass methods

  agda/agda2hs#411 · Filter by author HeinrichApfelmus opened on May 22, 2025
  1

• agda2hs locate doesn't work with the nix build

  nix
  agda/agda2hs#384 · Filter by author liesnikov opened on Dec 18, 2024

• agda2hs locate doesn't appear in the --help

  agda/agda2hs#383 · Filter by author liesnikov opened on Dec 18, 2024

• Incorrect transpilation of polymorphic where clauses

  error-reporting
  agda/agda2hs#362 · Filter by author HeinrichApfelmus opened on Sep 16, 2024
  12

• Support hiding things from the prelude

  enhancement
  agda/agda2hs#356 · Filter by author omelkonian opened on Sep 2, 2024