Code

Add Data.Nat.Bounded#2257

Code

Draft

jamesmckinna wants to merge 37 commits intoagda:masteragda/agda-stdlib:masterfrom jamesmckinna:bounded-natjamesmckinna/agda-stdlib:bounded-natCopy head branch name to clipboard

+390-1

Commits

Commits on Jan 15, 2024

• Add Data.Nat.Bounded

  jamesmckinna

  committed
  85c485f

  Copy full SHA for 85c485f

Commits on Jan 20, 2024

• renamed type; removed instance-based field; stumbled over isomorphism

  jamesmckinna

  committed
  92fa7e9

  Copy full SHA for 92fa7e9

• got there in the end: yuk!

  jamesmckinna

  committed
  f07cc16

  Copy full SHA for f07cc16

Commits on Jan 22, 2024

• added nonZeroIndex

  jamesmckinna

  committed
  dc8e53e

  Copy full SHA for dc8e53e

Commits on Jan 23, 2024

• added ℕ< literals

  jamesmckinna

  committed
  3d850f4

  Copy full SHA for 3d850f4

Commits on Jan 24, 2024

• added DecidableEquality

  jamesmckinna

  committed
  659d892

  Copy full SHA for 659d892

• too hasty to push

  jamesmckinna

  committed
  11bb699

  Copy full SHA for 11bb699

Commits on Jan 25, 2024

• added projection from Nat; additional constructors

  jamesmckinna

  committed
  51b6280

  Copy full SHA for 51b6280

• tweak to [[1]]<

  jamesmckinna

  committed
  04fae4f

  Copy full SHA for 04fae4f

Commits on Jan 28, 2024

• Merge branch 'master' into bounded-nat

  jamesmckinna

  authored
  32eb86b

  Copy full SHA for 32eb86b

Commits on Feb 1, 2024

• tweak

  jamesmckinna

  committed
  e560b6f

  Copy full SHA for e560b6f

Commits on Feb 4, 2024

• rename projection from Nat

  jamesmckinna

  committed
  0fe029e

  Copy full SHA for 0fe029e

Commits on Feb 5, 2024

• added Equivalence proof

  jamesmckinna

  committed
  6052c4f

  Copy full SHA for 6052c4f

• inverting fromℕ lemmas

  jamesmckinna

  committed
  821f51c

  Copy full SHA for 821f51c

• added quotient equivalence relation

  jamesmckinna

  committed
  194f122

  Copy full SHA for 194f122

Commits on Feb 9, 2024

• module refactoring

  jamesmckinna

  committed
  9a734c1

  Copy full SHA for 9a734c1

• cosmetic

  jamesmckinna

  committed
  dca2d54

  Copy full SHA for dca2d54

• added two simple lemmas about underlying values

  jamesmckinna

  committed
  823016b

  Copy full SHA for 823016b

Commits on Feb 10, 2024

• final lemma about the retraction

  jamesmckinna

  committed
  623d854

  Copy full SHA for 623d854

Commits on Feb 13, 2024

• tweaks to accomodate agda#2292

  jamesmckinna

  committed
  4076cc5

  Copy full SHA for 4076cc5

• additions to support agda#2292

  jamesmckinna

  committed
  f0f4883

  Copy full SHA for f0f4883

• refactored arithmetic

  jamesmckinna

  committed
  e1214bd

  Copy full SHA for e1214bd

Commits on Feb 14, 2024

• revised imports

  jamesmckinna

  committed
  10d4083

  Copy full SHA for 10d4083

Commits on Feb 26, 2024

• Merge branch 'master' into bounded-nat

  jamesmckinna

  authored
  771b501

  Copy full SHA for 771b501

Commits on Mar 8, 2024

• Merge branch 'master' into bounded-nat

  jamesmckinna

  authored
  8d523c8

  Copy full SHA for 8d523c8

Commits on Mar 17, 2024

• Merge branch 'master' into bounded-nat

  jamesmckinna

  authored
  9b4ee0e

  Copy full SHA for 9b4ee0e

• fixed up CHANGELOG

  jamesmckinna

  committed
  078d4f6

  Copy full SHA for 078d4f6

Commits on Mar 18, 2024

• Merge branch 'master' into bounded-nat

  jamesmckinna

  authored
  97f9cf9

  Copy full SHA for 97f9cf9

Commits on Mar 19, 2024

• Merge branch 'master' into bounded-nat

  jamesmckinna

  authored
  eccf88d

  Copy full SHA for eccf88d

Commits on May 6, 2024

• Merge branch 'master' into bounded-nat

  jamesmckinna

  authored
  f3e2550

  Copy full SHA for f3e2550

Commits on Jun 3, 2024

• Merge branch 'master' into bounded-nat

  jamesmckinna

  authored
  383529a

  Copy full SHA for 383529a

Commits on Jul 28, 2024

• update CHANGELOG to v2.2

  jamesmckinna

  committed
  3c3cbf3

  Copy full SHA for 3c3cbf3

• Merge branch 'agda:master' into bounded-nat

  jamesmckinna

  authored
  ba4e922

  Copy full SHA for ba4e922

• update CHANGELOG

  jamesmckinna

  committed
  00421a6

  Copy full SHA for 00421a6

Commits on Aug 3, 2024

• Merge branch 'master' into bounded-nat

  jamesmckinna

  authored
  49430b3

  Copy full SHA for 49430b3

Commits on Dec 7, 2024

• Merge branch 'agda:master' into bounded-nat

  jamesmckinna

  authored
  594d35c

  Copy full SHA for 594d35c

Commits on Dec 9, 2024

• Merge branch 'agda:master' into bounded-nat

  jamesmckinna

  authored
  716d585

  Copy full SHA for 716d585