Code

Simplify more Data.product imports#2014

Code

Merged

Taneb merged 3 commits intoagda:masteragda/agda-stdlib:masterfrom Saransh-cpp:Data.Product-take-2Saransh-cpp/agda-stdlib:Data.Product-take-2Copy head branch name to clipboardJul 28, 2023

Commits

Commits on Jul 3, 2023

• Simplify more Data.Product import to Data.Product.Base

  Saransh-cpp

  committed
  287678b

  Copy full SHA for 287678b

• Missed an import

  Saransh-cpp

  committed
  1816b6e

  Copy full SHA for 1816b6e

Commits on Jul 28, 2023

• Merge branch 'agda:master' into Data.Product-take-2

  Saransh-cpp

  authored
  f055bab

  Copy full SHA for f055bab