List view

Add <code>Data.Nat.Binary.Base.divMod</code>

addition

naming

Status: Closed (abandoned).

agda/agda-stdlibnumber 2029

#2029 In agda/agda-stdlib;

· by XiaohuWang0921 was closed on Nov 27, 2023

[ new ] associativity of Appending

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2023

#2023 In agda/agda-stdlib;

· by laMudri was closed on Feb 26, 2024

[ new ] symmetric core of a binary relation

addition

naming

Status: Merged (completed).

agda/agda-stdlibnumber 2071

#2071 In agda/agda-stdlib;

· by laMudri was closed on Feb 26, 2024

Added functional vector permutation

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2066

#2066 In agda/agda-stdlib;

· by guilhermehas was closed on Feb 25, 2024

Tidy up CHANGELOG in preparation for v2.1 release candidate

admin

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2412

#2412 In agda/agda-stdlib;

· by MatthewDaggitt was closed on Jun 19, 2024

Update LICENSE

admin

cosmetic

license

Status: Merged (completed).

agda/agda-stdlibnumber 2409

#2409 In agda/agda-stdlib;

· by lexvanderstoep was closed on Jun 16, 2024

[v2.1-rc1] Change quantification from implicit to explicit in <code>Algebra.Construct.Pointwise.liftRel</code>

library-design

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2433

#2433 In agda/agda-stdlib;

· by jamesmckinna was closed on Jul 7, 2024

[v2.1-rc1] fixes #2400: use explicit quantification instead

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2429

#2429 In agda/agda-stdlib;

· by jamesmckinna was closed on Jul 5, 2024

Fix v2.1-rc1 by reverting (some) changes to <code>Data.List.*</code>

bug

Status: Merged (completed).

agda/agda-stdlibnumber 2423

#2423 In agda/agda-stdlib;

· by jamesmckinna was closed on Jul 5, 2024

Refactor <code>Data.Sum.{to|from}Dec</code> via move+deprecate in <code>Relation.Nullary.Decidable.Core</code>

dependencies

library-design

low-hanging-fruit

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2405

#2405 In agda/agda-stdlib;

· by jamesmckinna was closed on Jun 17, 2024

fixes #2411

naming

Status: Merged (completed).

agda/agda-stdlibnumber 2413

#2413 In agda/agda-stdlib;

· by jamesmckinna was closed on Jun 19, 2024

Algebra fixity

documentation

library-design

Status: Merged (completed).

agda/agda-stdlibnumber 2386

#2386 In agda/agda-stdlib;

· by JacquesCarette was closed on May 16, 2024

Add <code>Data.List.Relation.Binary.Sublist.Setoid</code> categorical properties

addition

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2385

#2385 In agda/agda-stdlib;

· by jamesmckinna was closed on May 15, 2024

Refactor <code>Data.List.Base.scan*</code> and their properties

addition

dependencies

deprecation

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2395

#2395 In agda/agda-stdlib;

· by jamesmckinna was closed on May 30, 2024

Very dependent map

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2373

#2373 In agda/agda-stdlib;

· by JacquesCarette was closed on Jun 5, 2024

Add the <code>Setoid</code>-based <code>Monoid</code> on <code>(List, [], _++_)</code>

addition

library-design

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2393

#2393 In agda/agda-stdlib;

· by jamesmckinna was closed on May 30, 2024

<code>Data.List.Base.reverse</code> is self adjoint wrt <code>Data.List.Relation.Binary.Subset.Setoid._⊆_</code>

addition

low-hanging-fruit

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2378

#2378 In agda/agda-stdlib;

· by jamesmckinna was closed on May 13, 2024

Refactor <code>Function.Relation.Binary.Setoid.Equality</code> to lift out <code>isEquivalence</code>

addition

cosmetic

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2382

#2382 In agda/agda-stdlib;

· by jamesmckinna was closed on May 8, 2024

fixes #2375

addition

low-hanging-fruit

Status: Merged (completed).

agda/agda-stdlibnumber 2377

#2377 In agda/agda-stdlib;

· by jamesmckinna was closed on May 14, 2024

Pointwise <code>Algebra</code>

addition

low-hanging-fruit

Status: Merged (completed).

agda/agda-stdlibnumber 2381

#2381 In agda/agda-stdlib;

· by jamesmckinna was closed on May 15, 2024

Some properties of upTo and downFrom

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2316

#2316 In agda/agda-stdlib;

· by Taneb was closed on Mar 12, 2024

Refactor proofs from #2023

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2301

#2301 In agda/agda-stdlib;

· by jamesmckinna was closed on Feb 27, 2024

lemmas about semiring structure induced by <code>_× x</code>

addition

cosmetic

dependencies

deprecation

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2272

#2272 In agda/agda-stdlib;

· by jamesmckinna was closed on Feb 5, 2024

Qualified import of <code>Data.Product.Base</code> fixing #2280

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2284

#2284 In agda/agda-stdlib;

· by jamesmckinna was closed on Feb 8, 2024

Qualified import of reasoning modules fixing #2280

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2282

#2282 In agda/agda-stdlib;

· by jamesmckinna was closed on Feb 8, 2024