Code

Add Algebra.Action.* and friends#2350

Code

Draft

jamesmckinna wants to merge 37 commits intoagda:masteragda/agda-stdlib:masterfrom jamesmckinna:monoid-actionjamesmckinna/agda-stdlib:monoid-actionCopy head branch name to clipboard

+364

Commits

Commits on Apr 2, 2024

• beginnings

  jamesmckinna

  committed
  b9845ce

Commits on Apr 9, 2024

• factored out MonoidAction

  jamesmckinna

  committed
  43c9fdb

• second beginning

  jamesmckinna

  committed
  a503156

• start small(er)

  jamesmckinna

  committed
  e2a9815

• fix-whitespace

  jamesmckinna

  committed
  d9e6bc0

Commits on Apr 11, 2024

• refactor in favour of Pointwise congruence

  jamesmckinna

  committed
  d7a4ceb

• begin refactoring

  jamesmckinna

  committed
  aa6788e

• more refactoring

  jamesmckinna

  committed
  48a79e5

• more refactoring

  jamesmckinna

  committed
  56d9902

• factored out regular and free monoid actions

  jamesmckinna

  committed
  ace7e4d

• nearly there

  jamesmckinna

  committed
  d579e31

• little by little...

  jamesmckinna

  committed
  361ac24

• Self just needs tidying up: Biased smart constructor

  jamesmckinna

  committed
  160837f

• temp commit

  jamesmckinna

  committed
  8d0ed22

• fixed Free

  jamesmckinna

  committed
  a5995f3

• refactored Self

  jamesmckinna

  committed
  0eebed1

• fix-whitespace

  jamesmckinna

  committed
  8be311d

• tidy up!

  jamesmckinna

  committed
  47a5e71

Commits on Apr 12, 2024

• some response to review comments: give up on Raw structures; tweak notation; more modularisation for generality

  jamesmckinna

  committed
  364925d

• fixed comment

  jamesmckinna

  committed
  110d576

• removed more qualifications

  jamesmckinna

  committed
  63ef07e

• long opening comment on naming added

  jamesmckinna

  committed
  2f2c9b9

Commits on Apr 25, 2024

• notation

  jamesmckinna

  committed
  8e6b130

• flip notation; simplify Bundles

  jamesmckinna

  committed
  c0aa8b6

• congruence for List⁺ actions

  jamesmckinna

  committed
  79728c5

• simplify Self actions

  jamesmckinna

  committed
  937823d

• renamed Free to FreeMonoid: needs simplifying!

  jamesmckinna

  committed
  654eda0

• fix-up

  jamesmckinna

  committed
  04c535d

Commits on Apr 29, 2024

• tidied up FreeMonoid

  jamesmckinna

  committed
  305173d

• open API more eagerly

  jamesmckinna

  committed
  5702c46

• fix-whitespace

  jamesmckinna

  committed
  f1f73bf

Commits on May 1, 2024

• things in their right places, now

  jamesmckinna

  committed
  7df8e8c

• rethink notation

  jamesmckinna

  committed
  753e216

• knock-on

  jamesmckinna

  committed
  7570960

• tightened up dependencies

  jamesmckinna

  committed
  3981c4c

Commits on May 3, 2024

• inline uses of ListAction

  jamesmckinna

  committed
  2e292e7

Commits on May 8, 2024

• refactored to streamline FreeMonoid's use of iterated List actions

  jamesmckinna

  committed
  9b775da