Code

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

Code

Open

Taneb wants to merge 3 commits intomasteragda/agda-stdlib:masterfrom fast-totalagda/agda-stdlib:fast-totalCopy head branch name to clipboard

+15-8

Commits

Commits on Sep 2, 2024

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

  Taneb

  committed
  891f00e

  Copy full SHA for 891f00e

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

  Taneb

  committed
  68769e2

  Copy full SHA for 68769e2

• Update changelog

  Taneb

  committed
  165fd71

  Copy full SHA for 165fd71