Skip to content

Agda v2.8.0

New issue
Open
No due date
Last updated Mar 11, 2025
25% complete

List view

0 issues of 3 selected

  • Replace record directive "eta-equality" by "no-eta-equality;pattern"

    breaking
    status: blocked-by-issueProgress on this issue or PR is blocked by another issue.
    upstreamChanges induced by Agda upstream
    Status: Draft (not ready).
    agda/agda-stdlibnumber 2476
    #2476 In agda/agda-stdlib;
    · andreasabel opened on Sep 6, 2024

  • Problem with <code>DISPLAY</code> pragma for <code>⊥</code> in <code>Data.Empty</code>

    bug
    status: blocked-by-issueProgress on this issue or PR is blocked by another issue.
    upstreamChanges induced by Agda upstream
    Status: Open.
    #2493 In agda/agda-stdlib;
    · jamesmckinna opened on Oct 4, 2024

  • Fragile <code>NonZero</code> and implementation-dependent luck

    breaking
    bug
    instances
    Status: Open.
    #2644 In agda/agda-stdlib;
    · JacquesCarette opened on Mar 5, 2025
    •