List view

[ refactor ] cosmetic improvement to Algebra.Construct.Initial

addition

cosmetic

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2759

#2759 In agda/agda-stdlib;

· by jamesmckinna was closed on Jul 11, 2025

[Add] Consequences of associativity for Semigroups

addition

discussion

library-design

naming

Status: Merged (completed).

agda/agda-stdlibnumber 2688

#2688 In agda/agda-stdlib;

· by jmougeot was closed on Jul 2, 2025

Switch to Agda 2.8.0-rc3 by merging experimental into master

admin

Status: Merged (completed).

agda/agda-stdlibnumber 2755

#2755 In agda/agda-stdlib;

· by MatthewDaggitt was closed on Jun 30, 2025

[ refactor ] Restate, and use, the definitions of Monotonic etc. operations

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2580

#2580 In agda/agda-stdlib;

· by jamesmckinna was closed on Jul 3, 2025

Lemmata for if_then_else_

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2747

#2747 In agda/agda-stdlib;

· by pmbittner was closed on Jul 2, 2025

Adds Algebra.Morphism.Construct.DirectProduct

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2715

#2715 In agda/agda-stdlib;

· by carlostome was closed on Jul 2, 2025

Proved sorted permutations are equal

addition

documentation

Status: Merged (completed).

agda/agda-stdlibnumber 2748

#2748 In agda/agda-stdlib;

· by MatthewDaggitt was closed on Jul 2, 2025

[ add ] Relation.Binary.Properties.PartialSetoid

addition

naming

Status: Merged (completed).

agda/agda-stdlibnumber 2678

#2678 In agda/agda-stdlib;

· by jamesmckinna was closed on Jun 17, 2025

Correct option --warn to --warning for agda/agda#7966

upstreamChanges induced by Agda upstreamChanges induced by Agda upstream

Status: Merged (completed).

agda/agda-stdlibnumber 2754

#2754 In agda/agda-stdlib;

· by andreasabel was closed on Jun 28, 2025

Some preparatory proofs for proving sorting+permutation is equality

addition

Status: Closed (abandoned).

agda/agda-stdlibnumber 2724

#2724 In agda/agda-stdlib;

· by MatthewDaggitt was closed on Jun 2, 2025

[ add ] Reflects for unit and empty types

addition

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2727

#2727 In agda/agda-stdlib;

· by jamesmckinna was closed on Jun 4, 2025

Update CI

continuous-integration

Status: Merged (completed).

agda/agda-stdlibnumber 2544

#2544 In agda/agda-stdlib;

· by andreasabel was closed on Jan 18, 2025

[ refactor ] Remove use of rewrite from Data.List.Membership.Propositional.Properties.Core

cosmetic

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2548

#2548 In agda/agda-stdlib;

· by jamesmckinna was closed on Jan 15, 2025

Rename overloaded sym in apartness

bug

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2576

#2576 In agda/agda-stdlib;

· by bsaul was closed on Feb 19, 2025

[ refactor ] Data.List.Relation.Unary.Enumerates.Setoid.Properties using tighter lemma from Function.Consequences

cosmetic

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2574

#2574 In agda/agda-stdlib;

· by jamesmckinna was closed on Feb 12, 2025

[ refactor ] Axiom.ExcludedMiddle and Axiom.DoubleNegationElimination

cosmetic

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2575

#2575 In agda/agda-stdlib;

· by jamesmckinna was closed on Feb 7, 2025

[ bug ] Fix use of + in lemma preconditions in favour of ∧ (bis)

cosmetic

deprecation

refactoring

style-guide

Status: Merged (completed).

agda/agda-stdlibnumber 2578

#2578 In agda/agda-stdlib;

· by jamesmckinna was closed on Feb 9, 2025

[ refactor ] rename ∣∣ to ∥, ∤∤ to ∦ throughout Algebra.Definitions.RawMagma and Algebra.Properties.*.Divisibility

deprecation

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2562

#2562 In agda/agda-stdlib;

· by jamesmckinna was closed on Jan 23, 2025

[ refactor ] Add Data.Nat.ListAction

addition

dependencies

deprecation

library-design

naming

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2558

#2558 In agda/agda-stdlib;

· by jamesmckinna was closed on Feb 11, 2025

Add a few algebraic structures missing from the Algebra.Construct.Pointwise

addition

Status: Merged (completed).

agda/agda-stdlibnumber 2555

#2555 In agda/agda-stdlib;

· by bsaul was closed on Jan 19, 2025

Update documentation from v2.2 release version to v2.3-dev

admin

documentation

Status: Merged (completed).

agda/agda-stdlibnumber 2557

#2557 In agda/agda-stdlib;

· by jamesmckinna was closed on Jan 18, 2025

[ add ] Relation.Binary._Reflects_⟶_ as a companion to _Preserves_⟶_

addition

refactoring

Status: Closed (abandoned).

agda/agda-stdlibnumber 2566

#2566 In agda/agda-stdlib;

· by jamesmckinna was closed on Feb 12, 2025

[ refactor ] deprecate Algebra.Structures.IsGroup.{uniqueˡ-⁻¹|uniqueʳ-⁻¹} with knock-ons for Algebra.Module.*

deprecation

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2571

#2571 In agda/agda-stdlib;

· by jamesmckinna was closed on Mar 31, 2025

[ refactor ] Add Data.Bool.ListAction

addition

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 2561

#2561 In agda/agda-stdlib;

· by jamesmckinna was closed on Feb 5, 2025

[ bug ] Fix use of + in lemma preconditions in favour of ∧

bug

cosmetic

deprecation

Status: Merged (completed).

agda/agda-stdlibnumber 2564

#2564 In agda/agda-stdlib;

· by jamesmckinna was closed on Jan 25, 2025