Code

fixes #2408#2422

Code

Merged

jamesmckinna merged 4 commits intoagda:masteragda/agda-stdlib:masterfrom jamesmckinna:issue2408jamesmckinna/agda-stdlib:issue2408Copy head branch name to clipboardAug 2, 2024

+43

Commits

Commits on Jul 1, 2024

• fixes agda#2408

  jamesmckinna

  committed
  cc6a8e7

  Copy full SHA for cc6a8e7

Commits on Jul 4, 2024

• 'better' names?

  jamesmckinna

  committed
  e5f7424

  Copy full SHA for e5f7424

Commits on Jul 26, 2024

• added CHANGELOG entry

  jamesmckinna

  committed
  3a3219e

  Copy full SHA for 3a3219e

Commits on Jul 27, 2024

• Merge branch 'master' into issue2408

  jamesmckinna

  authored
  ef00bb2

  Copy full SHA for ef00bb2