List view

Added Z mod n as Fin

addition

Status: Closed (abandoned).

agda/agda-stdlibnumber 2073

#2073 In agda/agda-stdlib;

· by guilhermehas was closed on Dec 6, 2024

[ new ] notions of finiteness

addition

naming

Status: Closed (abandoned).

agda/agda-stdlibnumber 2022

#2022 In agda/agda-stdlib;

· by Saransh-cpp was closed on Dec 6, 2024

Add a property relating <code>maybe</code> to composition

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2414

#2414 In agda/agda-stdlib;

· by WhatisRT was closed on Sep 1, 2024

[ new ] map-concat

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2453

#2453 In agda/agda-stdlib;

· by gallais was closed on Aug 2, 2024

Vec.Properties: drop eq parameter when it is a property

deprecation

naming

Status: Merged (completed).

agda/agda-stdlibnumber 2430

#2430 In agda/agda-stdlib;

· by mildsunrise was closed on Aug 14, 2024

remove unnecessary condition in the <code>Relation.Binary.Reasoning.Base.Apartness</code>

bug

naming

Status: Merged (completed).

agda/agda-stdlibnumber 2438

#2438 In agda/agda-stdlib;

· by damhiya was closed on Aug 14, 2024

Fix #2443 by adding link to versioning table in installation instructions

addition

documentation

Status: Merged (completed).

agda/agda-stdlibnumber 2445

#2445 In agda/agda-stdlib;

· by MatthewDaggitt was closed on Jul 29, 2024

Run CI tests on release branches as well

admin

Status: Merged (completed).

agda/agda-stdlibnumber 2444

#2444 In agda/agda-stdlib;

· by MatthewDaggitt was closed on Aug 20, 2024

Added AVL.Map suggestion, explanation of MkValue args.

addition

documentation

Status: Merged (completed).

agda/agda-stdlibnumber 2447

#2447 In agda/agda-stdlib;

· by mars0i was closed on Aug 14, 2024

Refactor <code>Algebra.Solver.*Monoid</code>

breaking

dependencies

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2407

#2407 In agda/agda-stdlib;

· by jamesmckinna was closed on Sep 3, 2024

fixes #2408

addition

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2422

#2422 In agda/agda-stdlib;

· by jamesmckinna was closed on Aug 2, 2024

Vec.Properties: introduce <code>≈-cong′</code>

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2424

#2424 In agda/agda-stdlib;

· by mildsunrise was closed on Jan 3, 2025

Add proofs on truth value

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2418

#2418 In agda/agda-stdlib;

· by mildsunrise was closed on Aug 14, 2024

Add some type relations and isomorphisms

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2419

#2419 In agda/agda-stdlib;

· by WhatisRT was closed on Dec 6, 2024

Add left- and right- <code>Pointwise</code> congruence for <code>_++_</code> on <code>List</code>

addition

discussion

library-design

Status: Merged (completed).

agda/agda-stdlibnumber 2426

#2426 In agda/agda-stdlib;

· by jamesmckinna was closed on Aug 14, 2024

add <code>search</code> function to <code>Data.List.Relation.Unary.All</code>

addition

low-hanging-fruit

Status: Merged (completed).

agda/agda-stdlibnumber 2428

#2428 In agda/agda-stdlib;

· by jamesmckinna was closed on Aug 14, 2024

Add a couple lemmas about product in Data.List.Properties

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2460

#2460 In agda/agda-stdlib;

· by dolio was closed on Aug 22, 2024

Setup for v2.2 development

admin

Status: Merged (completed).

agda/agda-stdlibnumber 2439

#2439 In agda/agda-stdlib;

· by MatthewDaggitt was closed on Jul 27, 2024

[refactor] simplify dependencies

cosmetic

dependencies

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2455

#2455 In agda/agda-stdlib;

· by jamesmckinna was closed on Aug 12, 2024

Proof that <code>pred</code> is right adjoint to <code>suc</code> on <code>ℕ._≤_</code>

addition

cosmetic

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2456

#2456 In agda/agda-stdlib;

· by jamesmckinna was closed on Aug 15, 2024

[ add ] layout + boilerplate for deprecation warnings

addition

admin

style-guide

Status: Merged (completed).

agda/agda-stdlibnumber 2529

#2529 In agda/agda-stdlib;

· by jamesmckinna was closed on Dec 27, 2024

[ add ] Module <code>⊆-Reasoning</code> for <code>Data.List.Relation.Binary.Sublist.*</code>

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2527

#2527 In agda/agda-stdlib;

· by jamesmckinna was closed on Jan 3, 2025

Add <code>≤‴-irrelevant</code> to <code>Data.Nat.Properties</code>

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2503

#2503 In agda/agda-stdlib;

· by tsung-ju was closed on Dec 2, 2024

Add filter-≐

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2501

#2501 In agda/agda-stdlib;

· by Taneb was closed on Nov 19, 2024

Update installation instructions

admin

bug

documentation

Status: Merged (completed).

agda/agda-stdlibnumber 2512

#2512 In agda/agda-stdlib;

· by jamesmckinna was closed on Dec 9, 2024