Skip to content

Remove (almost!) all external use of _≤″_ beyond Data.Nat.*#2262

Merged
JacquesCarette merged 22 commits intoagda:masterfrom
jamesmckinna:vec-bounded-bis
Jun 17, 2024
Merged

Remove (almost!) all external use of `_≤″_` beyond `Data.Nat.*`#2262
JacquesCarette merged 22 commits intoagda:masterfrom
jamesmckinna:vec-bounded-bis

Commits

Commits on Jan 21, 2024

Commits on Feb 5, 2024

Commits on Mar 25, 2024

Commits on May 6, 2024

Commits on Jun 3, 2024

Commits on Jun 5, 2024

Commits on Jun 8, 2024