Code

Implement ≤-total in terms of _≤?_#2440

Code

Merged

jamesmckinna merged 4 commits intomasteragda/agda-stdlib:masterfrom fast-totalagda/agda-stdlib:fast-totalCopy head branch name to clipboardFeb 8, 2025

+15-8

Commits

Commits on Jan 30, 2025

• Define Data.Nat.≰⇒≥ directly and earlier

  Taneb

  committed
  098dc48

  Copy full SHA for 098dc48

• Define Data.Nat.≤-total in terms of _≤?_

  Taneb

  committed
  805a6f8

  Copy full SHA for 805a6f8

• Update changelog

  Taneb

  committed
  d8d2001

  Copy full SHA for d8d2001

• Be a bit lazier

  Taneb

  committed
  a8224d2

  Copy full SHA for a8224d2